ord_aleph0 — Mathlib

English

ord is injective in the sense that ord(a) = ord(b) iff a = b.

Русский

ord(a) = ord(b) тогда и только тогда, когда a = b.

LaTeX

$$$ \operatorname{ord}(a) = \operatorname{ord}(b) \iff a = b $$$

Lean4

@[simp]
theorem ord_aleph0 : ord.{u} ℵ₀ = ω :=
  by
  refine le_antisymm (ord_le.2 le_rfl) <| le_of_forall_lt fun o h ↦ ?_
  rcases Ordinal.lt_lift_iff.1 h with ⟨o, ho, rfl⟩
  rw [lt_ord, ← lift_card, lift_lt_aleph0, ← typein_enum _ ho]
  exact lt_aleph0_iff_fintype.2 ⟨Set.fintypeLTNat _⟩

Похожие утверждения