card_le_card — Mathlib

English

If a is initial, then a.card ≤ b.card iff a ≤ b.

Русский

Если a — начальный, то a.card ≤ b.card эквивалентно a ≤ b.

LaTeX

$$$\\\\forall a,b \\\\in \\\\text{Ordinal}, \\\\text{IsInitial}(a) \\\\Rightarrow a.card \\\\le b.card \\\\Leftrightarrow a \\\\le b.$$$

Lean4

theorem card_le_card {a b : Ordinal} (ha : IsInitial a) : a.card ≤ b.card ↔ a ≤ b :=
  by
  refine ⟨fun h ↦ ?_, Ordinal.card_le_card⟩
  rw [← ord_le_ord, ha.ord_card] at h
  exact h.trans (ord_card_le b)

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