feat(set_theory/cardinal/cofinality): limit cardinal is at least ω (#…

…14432)
leanprover-community · Jun 4, 2022 · 0746194 · 0746194
1 parent 15726ee
commit 0746194
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/src/set_theory/cardinal/cofinality.lean b/src/set_theory/cardinal/cofinality.lean
@@ -701,6 +701,14 @@ local infixr ^ := @pow cardinal.{u} cardinal cardinal.has_pow
 def is_limit (c : cardinal) : Prop :=
 c ≠ 0 ∧ ∀ x < c, succ x < c
 
+theorem is_limit.omega_le {c} (h : is_limit c) : ω ≤ c :=
+begin
+  by_contra' h',
+  rcases lt_omega.1 h' with ⟨_ | n, rfl⟩,
+  { exact h.1.irrefl },
+  { simpa using h.2 n }
+end
+
 /-- A cardinal is a strong limit if it is not zero and it is
   closed under powersets. Note that `ω` is a strong limit by this definition. -/
 def is_strong_limit (c : cardinal) : Prop :=