feat(set_theory/cardinal/ordinal): Beth numbers form a normal family (#…

…16853)

Prove `is_normal (λ o, (beth o).ord)`

src/set_theory/cardinal/ordinal.lean

@@ -364,6 +364,8 @@ begin
     exact le_csupr (bdd_above_of_small _) (⟨_, hb.succ_lt h⟩ : Iio b) }
 end
 
+lemma beth_mono : monotone beth := beth_strict_mono.monotone
+
 @[simp] theorem beth_lt {o₁ o₂ : ordinal} : beth o₁ < beth o₂ ↔ o₁ < o₂ :=
 beth_strict_mono.lt_iff_lt
 
@@ -391,6 +393,10 @@ aleph_0_pos.trans_le $ aleph_0_le_beth o
 theorem beth_ne_zero (o : ordinal) : beth o ≠ 0 :=
 (beth_pos o).ne'
 
+lemma beth_normal : is_normal.{u} (λ o, (beth o).ord) :=
+(is_normal_iff_strict_mono_limit _).2 ⟨ord_strict_mono.comp beth_strict_mono, λ o ho a ha,
+  by { rw [beth_limit ho, ord_le], exact csupr_le' (λ b, ord_le.1 (ha _ b.2)) }⟩
+
 /-! ### Properties of `mul` -/
 
 /-- If `α` is an infinite type, then `α × α` and `α` have the same cardinality. -/