feat(SetTheory): definition of initial ordinals, ω₁ as an ordinal, or…

…dinal-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 `iUnion`s in preparation for material on the Borel hierarchy.



Co-authored-by: Pedro Sánchez Terraf <sterraf@users.noreply.github.com>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/SetTheory/Cardinal/Cofinality.lean

@@ -1250,3 +1250,20 @@ theorem lt_cof_power {a b : Cardinal} (ha : ℵ₀ ≤ a) (b1 : 1 < b) : a < cof
 #align cardinal.lt_cof_power Cardinal.lt_cof_power
 
 end Cardinal
+
+section Omega1
+
+namespace Ordinal
+
+open Cardinal
+open scoped Ordinal
+
+lemma sup_sequence_lt_omega1 {α} [Countable α] (o : α → Ordinal) (ho : ∀ n, o n < ω₁) :
+    sup o < ω₁ := by
+  apply sup_lt_ord_lift _ ho
+  rw [Cardinal.isRegular_aleph_one.cof_eq]
+  exact lt_of_le_of_lt mk_le_aleph0 aleph0_lt_aleph_one
+
+end Ordinal
+
+end Omega1

Mathlib/SetTheory/Cardinal/Ordinal.lean

@@ -24,7 +24,9 @@ using ordinals.
   It is an order isomorphism between ordinals and cardinals.
 * The function `Cardinal.aleph` gives the infinite cardinals listed by their
   ordinal index. `aleph 0 = ℵ₀`, `aleph 1 = succ ℵ₀` is the first
-  uncountable cardinal, and so on.
+  uncountable cardinal, and so on. The notation `ω_` combines the latter with `Cardinal.ord`,
+  giving an enumeration of (infinite) initial ordinals.
+  Thus `ω_ 0 = ω` and `ω₁ = ω_ 1` is the first uncountable ordinal.
 * The function `Cardinal.beth` enumerates the Beth cardinals. `beth 0 = ℵ₀`,
   `beth (succ o) = 2 ^ beth o`, and for a limit ordinal `o`, `beth o` is the supremum of `beth a`
   for `a < o`.
@@ -1446,3 +1448,46 @@ theorem extend_function_of_lt {α β : Type*} {s : Set α} (f : s ↪ β) (hs :
 -- end Bit
 
 end Cardinal
+
+section Initial
+
+namespace Ordinal
+
+/--
+`ω_ o` is a notation for the *initial ordinal* of cardinality
+`aleph o`. Thus, for example `ω_ 0 = ω`.
+-/
+scoped notation "ω_" o => ord <| aleph o
+
+/--
+`ω₁` is the first uncountable ordinal.
+-/
+scoped notation "ω₁" => ord <| aleph 1
+
+lemma omega_lt_omega1 : ω < ω₁ := ord_aleph0.symm.trans_lt (ord_lt_ord.mpr (aleph0_lt_aleph_one))
+
+section OrdinalIndices
+/-!
+### Cardinal operations with ordinal indices
+
+Results on cardinality of ordinal-indexed families of sets.
+-/
+namespace Cardinal
+
+open scoped Cardinal
+
+/--
+Bounding the cardinal of an ordinal-indexed union of sets.
+-/
+lemma mk_iUnion_Ordinal_le_of_le {β : Type _} {o : Ordinal} {c : Cardinal}
+    (ho : o.card ≤ c) (hc : ℵ₀ ≤ c) (A : Ordinal → Set β)
+    (hA : ∀ j < o, #(A j) ≤ c) :
+    #(⋃ j < o, A j) ≤ c := by
+  simp_rw [← mem_Iio, biUnion_eq_iUnion, iUnion, iSup, ← o.enumIsoOut.symm.surjective.range_comp]
+  apply ((mk_iUnion_le _).trans _).trans_eq (mul_eq_self hc)
+  rw [mk_ordinal_out]
+  exact mul_le_mul' ho <| ciSup_le' <| (hA _ <| typein_lt_self ·)
+
+end Cardinal
+
+end OrdinalIndices

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -1378,6 +1378,19 @@ theorem lt_ord_succ_card (o : Ordinal) : o < (succ o.card).ord :=
   lt_ord.2 <| lt_succ _
 #align cardinal.lt_ord_succ_card Cardinal.lt_ord_succ_card
 
+theorem card_le_iff {o : Ordinal} {c : Cardinal} : o.card ≤ c ↔ o < (succ c).ord := by
+  rw [lt_ord, lt_succ_iff]
+
+/--
+A variation on `Cardinal.lt_ord` using `≤`: If `o` is no greater than the
+initial ordinal of cardinality `c`, then its cardinal is no greater than `c`.
+
+The converse, however, is false (for instance, `o = ω+1` and `c = ℵ₀`).
+-/
+lemma card_le_of_le_ord {o : Ordinal} {c : Cardinal} (ho : o ≤ c.ord) :
+    o.card ≤ c := by
+  rw [← card_ord c]; exact Ordinal.card_le_card ho
+
 @[mono]
 theorem ord_strictMono : StrictMono ord :=
   gciOrdCard.strictMono_l