isNormal_ord — Mathlib

English

Ordinal map ord is injective: if ord(a) = ord(b) then a = b.

Русский

Упорядоченное отображение ord инъективно: ord(a) = ord(b) ⇒ a = b.

LaTeX

$$$ \forall a,b\, (\operatorname{ord}(a) = \operatorname{ord}(b)) \Rightarrow a = b $$$

Lean4

theorem isNormal_ord : Order.IsNormal ord where
  strictMono := ord_strictMono
  mem_lowerBounds_upperBounds_of_isSuccLimit := by
    intro a ha
    simp_rw [lowerBounds, upperBounds, mem_setOf, forall_mem_image, ord_le]
    refine fun b H ↦ le_of_forall_lt fun c hc ↦ ?_
    simpa using H (ha.succ_lt hc)

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