feat(set_theory/cardinal/cofinality): ω is a strong limit cardinal (#…

…14436)

src/set_theory/cardinal/cofinality.lean

@@ -714,9 +714,18 @@ end
 def is_strong_limit (c : cardinal) : Prop :=
 c ≠ 0 ∧ ∀ x < c, 2 ^ x < c
 
+theorem is_strong_limit_omega : is_strong_limit ω :=
+⟨omega_ne_zero, λ x hx, begin
+  rcases lt_omega.1 hx with ⟨n, rfl⟩,
+  exact_mod_cast nat_lt_omega (pow 2 n)
+end⟩
+
 theorem is_strong_limit.is_limit {c} (H : is_strong_limit c) : is_limit c :=
 ⟨H.1, λ x h, lt_of_le_of_lt (succ_le_of_lt $ cantor x) (H.2 _ h)⟩
 
+theorem is_limit_omega : is_limit ω :=
+is_strong_limit_omega.is_limit
+
 /-- A cardinal is regular if it is infinite and it equals its own cofinality. -/
 def is_regular (c : cardinal) : Prop :=
 ω ≤ c ∧ c.ord.cof = c