### 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.

### License

BSD License

### Topics

- Mathematics/Combinatorics
- Logic/Set theory

### Session Delta_System_Lemma

- ZF_Library
- Cofinality
- Cardinal_Library
- Konig
- Delta_System
- Cohen_Posets

### Used by

- Transitive Models of Fragments of ZFC

## Cite

×

Delta_System_Lemma-AFP

    @article{Delta_System_Lemma-AFP,
      author  = {Pedro Sánchez Terraf},
      title   = {Cofinality and the Delta System Lemma},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Delta_System_Lemma.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Dec 28, 2020 : Isabelle2020