feat(set_theory/ordinal/basic): order type of naturals is ω (#15178)

leanprover-community · Jul 9, 2022 · 6d245b2 · 6d245b2
1 parent 7cf0ae6
commit 6d245b2
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/set_theory/ordinal/basic.lean b/src/set_theory/ordinal/basic.lean
@@ -926,6 +926,9 @@ def omega : ordinal.{u} := lift $ @type ℕ (<) _
 
 localized "notation `ω` := ordinal.omega" in ordinal
 
+/-- Note that the presence of this lemma makes `simp [omega]` form a loop. -/
+@[simp] theorem type_nat_lt : @type ℕ (<) _ = ω := (lift_id _).symm
+
 @[simp] theorem card_omega : card ω = ℵ₀ := rfl
 
 @[simp] theorem lift_omega : lift ω = ω := lift_lift _