Commit 2023-09-03 17:06 58a5282e

View on Github →

feat(SetTheory): definition of initial ordinals, ω₁ as an ordinal, ordinal-indexed unions (#6404)

  • I setup notation for the first ordinal in each cardinality.
  • ω₁ is defined as an ordinal, not as an out (cf. MeasureTheory.CardMeasurableSpace).
  • Lemma using the cofinality of ω₁.
  • Lemma on the cardinality of ordinal-indexed iUnions in preparation for material on the Borel hierarchy.

Estimated changes

added theorem Cardinal.card_le_iff