feat(SetTheory/Cardinal/Aleph): define initial ordinals (#16964)

Author: vihdzp

Mathlib/SetTheory/Cardinal/Aleph.lean

@@ -41,10 +41,65 @@ open Function Set Cardinal Equiv Order Ordinal
 
 universe u v w
 
-namespace Cardinal
+/-! ### Omega ordinals -/
+
+namespace Ordinal
+
+/-- An ordinal is initial when it is the first ordinal with a given cardinality.
+
+This is written as `o.card.ord = o`, i.e. `o` is the smallest ordinal with cardinality `o.card`. -/
+def IsInitial (o : Ordinal) : Prop :=
+  o.card.ord = o
+
+theorem IsInitial.ord_card {o : Ordinal} (h : IsInitial o) : o.card.ord = o := h
+
+theorem IsInitial.card_le_card {a b : Ordinal} (ha : IsInitial a) : a.card ≤ b.card ↔ a ≤ b := by
+  refine ⟨fun h ↦ ?_, Ordinal.card_le_card⟩
+  rw [← ord_le_ord, ha.ord_card] at h
+  exact h.trans (ord_card_le b)
+
+theorem IsInitial.card_lt_card {a b : Ordinal} (hb : IsInitial b) : a.card < b.card ↔ a < b :=
+  lt_iff_lt_of_le_iff_le hb.card_le_card
+
+theorem isInitial_ord (c : Cardinal) : IsInitial c.ord := by
+  rw [IsInitial, card_ord]
+
+theorem isInitial_natCast (n : ℕ) : IsInitial n := by
+  rw [IsInitial, card_nat, ord_nat]
+
+theorem isInitial_zero : IsInitial 0 := by
+  exact_mod_cast isInitial_natCast 0
+
+theorem isInitial_one : IsInitial 1 := by
+  exact_mod_cast isInitial_natCast 1
+
+theorem isInitial_omega0 : IsInitial ω := by
+  rw [IsInitial, card_omega0, ord_aleph0]
+
+theorem not_bddAbove_isInitial : ¬ BddAbove {x | IsInitial x} := by
+  rintro ⟨a, ha⟩
+  have := ha (isInitial_ord (succ a.card))
+  rw [ord_le] at this
+  exact (lt_succ _).not_le this
+
+/-- Initial ordinals are order-isomorphic to the cardinals. -/
+@[simps!]
+def isInitialIso : {x // IsInitial x} ≃o Cardinal where
+  toFun x := x.1.card
+  invFun x := ⟨x.ord, isInitial_ord _⟩
+  left_inv x := Subtype.ext x.2.ord_card
+  right_inv x := card_ord x
+  map_rel_iff' {a _} := a.2.card_le_card
+
+-- TODO: define `omega` as the enumerator function of `IsInitial`, and redefine
+-- `aleph x = (omega x).card`.
+
+end Ordinal
 
 /-! ### Aleph cardinals -/
 
+namespace Cardinal
+
 /-- The `aleph'` function gives the cardinals listed by their ordinal index. `aleph' n = n`,
 `aleph' ω = ℵ₀`, `aleph' (ω + 1) = succ ℵ₀`, etc.
 

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -2219,14 +2219,6 @@ namespace Cardinal
 
 open Ordinal
 
-@[simp]
-theorem ord_aleph0 : ord.{u} ℵ₀ = ω :=
-  le_antisymm (ord_le.2 <| le_rfl) <|
-    le_of_forall_lt fun o h => by
-      rcases Ordinal.lt_lift_iff.1 h with ⟨o, rfl, h'⟩
-      rw [lt_ord, ← lift_card, lift_lt_aleph0, ← typein_enum (· < ·) h']
-      exact lt_aleph0_iff_fintype.2 ⟨Set.fintypeLTNat _⟩
-
 @[simp]
 theorem add_one_of_aleph0_le {c} (h : ℵ₀ ≤ c) : c + 1 = c := by
   rw [add_comm, ← card_ord c, ← card_one, ← card_add, one_add_of_omega0_le]

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -1214,6 +1214,14 @@ theorem ord_one : ord 1 = 1 := by simpa using ord_nat 1
 theorem ord_ofNat (n : ℕ) [n.AtLeastTwo] : ord (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
   ord_nat n
 
+@[simp]
+theorem ord_aleph0 : ord.{u} ℵ₀ = ω :=
+  le_antisymm (ord_le.2 le_rfl) <|
+    le_of_forall_lt fun o h => by
+      rcases Ordinal.lt_lift_iff.1 h with ⟨o, rfl, h'⟩
+      rw [lt_ord, ← lift_card, lift_lt_aleph0, ← typein_enum (· < ·) h']
+      exact lt_aleph0_iff_fintype.2 ⟨Set.fintypeLTNat _⟩
+
 @[simp]
 theorem lift_ord (c) : Ordinal.lift.{u,v} (ord c) = ord (lift.{u,v} c) := by
   refine le_antisymm (le_of_forall_lt fun a ha => ?_) ?_