Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-2020
Commits
2da14e4d854f
Commit
b77db792
authored
Dec 28, 2020
by
Lawrence Paulson
Browse files
webpage for Delta_System_Lemma
parent
89ed1831f6cd
Changes
7
Expand all
Hide whitespace changes
Inline
Side-by-side
metadata/metadata
View file @
2da14e4d
...
...
@@ -9593,6 +9593,19 @@ abstract =
transitive model of ZFC, we construct a proper generic extension and
show that the latter also satisfies ZFC.
[Delta_System_Lemma]
title = Cofinality and the Delta System Lemma
author = Pedro Sánchez Terraf <https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
topic = Mathematics/Combinatorics, Logic/Set theory
date = 2020-12-27
notify = sterraf@famaf.unc.edu.ar
abstract =
We formalize the basic results on cofinality of linearly ordered sets
and ordinals and Šanin’s Lemma for uncountable families of finite
sets. This last result is used to prove the countable chain condition
for Cohen posets. We work in the set theory framework of Isabelle/ZF,
using the Axiom of Choice as needed.
[Recursion-Addition]
title = Recursion Theorem in ZF
author = Georgy Dunaev <mailto:georgedunaev@gmail.com>
...
...
@@ -9960,7 +9973,7 @@ author = Walter Guttmann <http://www.cosc.canterbury.ac.nz/walter.guttmann/>, Ni
topic = Computer science/Algorithms/Graph
date = 2020-12-08
notify = walter.guttmann@canterbury.ac.nz
abstract =
abstract =
We verify the correctness of Prim's, Kruskal's and
Borůvka's minimum spanning tree algorithms based on algebras for
aggregation and minimisation.
...
...
@@ -9971,7 +9984,7 @@ author = David Fuenmayor <mailto:davfuenmayor@gmail.com>
topic = Logic/General logic
date = 2020-12-17
notify = davfuenmayor@gmail.com
abstract =
abstract =
We introduce a generalized topological semantics for paraconsistent
and paracomplete logics by drawing upon early works on topological
Boolean algebras (cf. works by Kuratowski, Zarycki, McKinsey &
...
...
web/entries/Delta_System_Lemma.html
0 → 100644
View file @
2da14e4d
<!DOCTYPE html>
<html
lang=
"en"
>
<head>
<meta
charset=
"utf-8"
>
<title>
Cofinality and the Delta System Lemma - Archive of Formal Proofs
</title>
<link
rel=
"stylesheet"
type=
"text/css"
href=
"../front.css"
>
<link
rel=
"icon"
href=
"../images/favicon.ico"
type=
"image/icon"
>
<link
rel=
"alternate"
type=
"application/rss+xml"
title=
"RSS"
href=
"../rss.xml"
>
<!-- MathJax for LaTeX support in abstracts -->
<script>
MathJax
=
{
tex
:
{
inlineMath
:
[[
'
$
'
,
'
$
'
],
[
'
\\
(
'
,
'
\\
)
'
]]
},
processEscapes
:
true
,
svg
:
{
fontCache
:
'
global
'
}
};
</script>
<script
id=
"MathJax-script"
async
src=
"../components/mathjax/es5/tex-mml-chtml.js"
></script>
</head>
<body
class=
"mathjax_ignore"
>
<table
width=
"100%"
>
<tbody>
<tr>
<!-- Navigation -->
<td
width=
"20%"
align=
"center"
valign=
"top"
>
<p>
</p>
<a
href=
"https://www.isa-afp.org/"
>
<img
src=
"../images/isabelle.png"
width=
"100"
height=
"88"
border=
0
>
</a>
<p>
</p>
<p>
</p>
<table
class=
"nav"
width=
"80%"
>
<tr>
<td
class=
"nav"
width=
"100%"
><a
href=
"../index.html"
>
Home
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../about.html"
>
About
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../submitting.html"
>
Submission
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../updating.html"
>
Updating Entries
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../using.html"
>
Using Entries
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../search.html"
>
Search
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../statistics.html"
>
Statistics
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../topics.html"
>
Index
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../download.html"
>
Download
</a></td>
</tr>
</table>
<p>
</p>
<p>
</p>
</td>
<!-- Content -->
<td
width=
"80%"
valign=
"top"
>
<div
align=
"center"
>
<p>
</p>
<h1>
<font
class=
"first"
>
C
</font>
ofinality
and
the
<font
class=
"first"
>
D
</font>
elta
<font
class=
"first"
>
S
</font>
ystem
<font
class=
"first"
>
L
</font>
emma
</h1>
<p>
</p>
<table
width=
"80%"
class=
"data"
>
<tbody>
<tr>
<td
class=
"datahead"
width=
"20%"
>
Title:
</td>
<td
class=
"data"
width=
"80%"
>
Cofinality and the Delta System Lemma
</td>
</tr>
<tr>
<td
class=
"datahead"
>
Author:
</td>
<td
class=
"data"
>
<a
href=
"https://cs.famaf.unc.edu.ar/~pedro/home_en.html"
>
Pedro Sánchez Terraf
</a>
</td>
</tr>
<tr>
<td
class=
"datahead"
>
Submission date:
</td>
<td
class=
"data"
>
2020-12-27
</td>
</tr>
<tr>
<td
class=
"datahead"
valign=
"top"
>
Abstract:
</td>
<td
class=
"abstract mathjax_process"
>
We formalize the basic results on cofinality of linearly ordered sets
and ordinals and Šanin’s Lemma for uncountable families of finite
sets. This last result is used to prove the countable chain condition
for Cohen posets. We work in the set theory framework of Isabelle/ZF,
using the Axiom of Choice as needed.
</td>
</tr>
<tr>
<td
class=
"datahead"
valign=
"top"
>
BibTeX:
</td>
<td
class=
"formatted"
>
<pre>
@article{Delta_System_Lemma-AFP,
author = {Pedro Sánchez Terraf},
title = {Cofinality and the Delta System Lemma},
journal = {Archive of Formal Proofs},
month = dec,
year = 2020,
note = {\url{https://isa-afp.org/entries/Delta_System_Lemma.html},
Formal proof development},
ISSN = {2150-914x},
}
</pre>
</td>
</tr>
<tr><td
class=
"datahead"
>
License:
</td>
<td
class=
"data"
><a
href=
"http://isa-afp.org/LICENSE"
>
BSD License
</a></td></tr>
</tbody>
</table>
<p></p>
<table
class=
"links"
>
<tbody>
<tr>
<td
class=
"links"
>
<a
href=
"../browser_info/current/AFP/Delta_System_Lemma/outline.pdf"
>
Proof outline
</a><br>
<a
href=
"../browser_info/current/AFP/Delta_System_Lemma/document.pdf"
>
Proof document
</a>
</td>
</tr>
<tr>
<td
class=
"links"
>
<a
href=
"../browser_info/current/AFP/Delta_System_Lemma/index.html"
>
Browse theories
</a>
</td></tr>
<tr>
<td
class=
"links"
>
<a
href=
"../release/afp-Delta_System_Lemma-current.tar.gz"
>
Download this entry
</a>
</td>
</tr>
<tr><td
class=
"links"
>
Older releases:
None
</td></tr>
</tbody>
</table>
</div>
</td>
</tr>
</tbody>
</table>
<script
src=
"../jquery.min.js"
></script>
<script
src=
"../script.js"
></script>
</body>
</html>
\ No newline at end of file
web/entries/Forcing.html
View file @
2da14e4d
...
...
@@ -101,7 +101,7 @@ MathJax = {
<td
class=
"data"
>
Emmanuel Gunther (gunther /at/ famaf /dot/ unc /dot/ edu /dot/ ar),
<a
href=
"https://cs.famaf.unc.edu.ar/~mpagano/"
>
Miguel Pagano
</a>
and
<a
href=
"https://cs.famaf.unc.edu.ar/~pedro/home_en"
>
Pedro Sánchez Terraf
</a>
<a
href=
"https://cs.famaf.unc.edu.ar/~pedro/home_en
.html
"
>
Pedro Sánchez Terraf
</a>
</td>
</tr>
...
...
web/index.html
View file @
2da14e4d
...
...
@@ -88,6 +88,14 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
<tr>
<td
class=
"head"
>
2020
</td>
</tr>
<tr>
<td
class=
"entry"
>
2020-12-27:
<a
href=
"entries/Delta_System_Lemma.html"
>
Cofinality and the Delta System Lemma
</a>
<br>
Author:
<a
href=
"https://cs.famaf.unc.edu.ar/~pedro/home_en.html"
>
Pedro Sánchez Terraf
</a>
</td>
</tr>
<tr>
<td
class=
"entry"
>
2020-12-17:
<a
href=
"entries/Topological_Semantics.html"
>
Topological semantics for paraconsistent and paracomplete logics
</a>
...
...
@@ -385,7 +393,7 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
Authors:
Emmanuel Gunther,
<a
href=
"https://cs.famaf.unc.edu.ar/~mpagano/"
>
Miguel Pagano
</a>
and
<a
href=
"https://cs.famaf.unc.edu.ar/~pedro/home_en"
>
Pedro Sánchez Terraf
</a>
and
<a
href=
"https://cs.famaf.unc.edu.ar/~pedro/home_en
.html
"
>
Pedro Sánchez Terraf
</a>
</td>
</tr>
<tr>
...
...
web/rss.xml
View file @
2da14e4d
...
...
@@ -9,7 +9,20 @@
and larger scientific developments, mechanically checked
in the theorem prover Isabelle.
</description>
<pubDate>
17 Dec 2020 00:00:00 +0000
</pubDate>
<pubDate>
27 Dec 2020 00:00:00 +0000
</pubDate>
<item>
<title>
Cofinality and the Delta System Lemma
</title>
<link>
https://www.isa-afp.org/entries/Delta_System_Lemma.html
</link>
<guid>
https://www.isa-afp.org/entries/Delta_System_Lemma.html
</guid>
<dc:creator>
Pedro Sánchez Terraf
</dc:creator>
<pubDate>
27 Dec 2020 00:00:00 +0000
</pubDate>
<description>
We formalize the basic results on cofinality of linearly ordered sets
and ordinals and Šanin’s Lemma for uncountable families of finite
sets. This last result is used to prove the countable chain condition
for Cohen posets. We work in the set theory framework of Isabelle/ZF,
using the Axiom of Choice as needed.
</description>
</item>
<item>
<title>
Topological semantics for paraconsistent and paracomplete logics
</title>
<link>
https://www.isa-afp.org/entries/Topological_Semantics.html
</link>
...
...
@@ -579,18 +592,5 @@ infinite sets of finite sets (or lists) subject to a “no initial
segment” condition. The present formalisation follows a
monograph on Ramsey Spaces by Todorčević.
</description>
</item>
<item>
<title>
A Formalization of Knuth–Bendix Orders
</title>
<link>
https://www.isa-afp.org/entries/Knuth_Bendix_Order.html
</link>
<guid>
https://www.isa-afp.org/entries/Knuth_Bendix_Order.html
</guid>
<dc:creator>
Christian Sternagel, René Thiemann
</dc:creator>
<pubDate>
13 May 2020 00:00:00 +0000
</pubDate>
<description>
We define a generalized version of Knuth
&
ndash;Bendix orders,
including subterm coefficient functions. For these orders we formalize
several properties such as strong normalization, the subterm property,
closure properties under substitutions and contexts, as well as ground
totality.
</description>
</item>
</channel>
</rss>
web/statistics.html
View file @
2da14e4d
This diff is collapsed.
Click to expand it.
web/topics.html
View file @
2da14e4d
...
...
@@ -570,6 +570,7 @@
<a
href=
"entries/HereditarilyFinite.html"
>
HereditarilyFinite
</a>
<a
href=
"entries/ZFC_in_HOL.html"
>
ZFC_in_HOL
</a>
<a
href=
"entries/Forcing.html"
>
Forcing
</a>
<a
href=
"entries/Delta_System_Lemma.html"
>
Delta_System_Lemma
</a>
<a
href=
"entries/Recursion-Addition.html"
>
Recursion-Addition
</a>
<a
href=
"entries/Ordinal_Partitions.html"
>
Ordinal_Partitions
</a>
</div>
...
...
@@ -866,6 +867,7 @@
<a
href=
"entries/Catalan_Numbers.html"
>
Catalan_Numbers
</a>
<a
href=
"entries/Falling_Factorial_Sum.html"
>
Falling_Factorial_Sum
</a>
<a
href=
"entries/Matroids.html"
>
Matroids
</a>
<a
href=
"entries/Delta_System_Lemma.html"
>
Delta_System_Lemma
</a>
<a
href=
"entries/Nash_Williams.html"
>
Nash_Williams
</a>
<a
href=
"entries/Ordinal_Partitions.html"
>
Ordinal_Partitions
</a>
</div>
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment