session Delta_System_Lemma = "ZF-Constructible" +
description " Cofinality and Delta System Lemma
We formalize the basic results on cofinality of linearly ordered sets and ordinals and Shanin'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. "
options [timeout = 600]
theories "Konig" "Delta_System" "Cohen_Posets"
document_files "root.tex" "header-delta-system.tex" "multidef.sty" "root.bib" "root.bst"
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.9 Sekunden
(vorverarbeitet am 2026-06-10)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
