rank_le_iff — Mathlib

English

rank x ≤ o if and only if every y ∈ x has rank(y) < o.

Русский

rank x ≤ o тогда и только тогда, когда для каждого y ∈ x rank(y) < o.

LaTeX

$$$\\\\forall {x}, {o} :\\\\ rank x \\\\le o \\\\iff \\\\forall y \\\\in x, rank(y) < o$$$

Lean4

theorem rank_le_iff {o : Ordinal} : rank x ≤ o ↔ ∀ ⦃y⦄, y ∈ x → rank y < o :=
  ⟨fun h _ h' => (rank_lt_of_mem h').trans_le h,
    Quotient.inductionOn x fun _ h => PSet.rank_le_iff.2 fun y h' => @h ⟦y⟧ h'⟩

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