| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Cofinality and the Delta System Lemma
| Title: | Cofinality and the Delta System Lemma |
| Author: | Pedro Sánchez Terraf |
| Submission date: | 2020-12-27 |
| 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. |
| BibTeX: |
@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},
}
|
| License: | BSD License |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |