Cofinality and the Delta System Lemma (Q7361960)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Delta_System_Lemma
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Cofinality and the Delta System Lemma |
AFP entry Delta_System_Lemma |
Statements
27 December 2020
0 references
Pedro Sánchez Terraf
0 references
Cofinality and the Delta System Lemma (English)
0 references
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.
0 references
