rank_le_iff — Mathlib

English

For every pre-set x and ordinal o, rank x ≤ o iff all elements y ∈ x have rank less than o.

Русский

Для каждого пред-множества x и ординара o, rank(x) ≤ o тогда и только тогда, когда все элементы y ∈ x имеют rank(y) < o.

LaTeX

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

Lean4

theorem rank_le_iff {o : Ordinal} : ∀ {x : PSet}, rank x ≤ o ↔ ∀ ⦃y⦄, y ∈ x → rank y < o
  | ⟨_, A⟩ => by
    refine ⟨fun h _ h' => (rank_lt_of_mem h').trans_le h, fun h ↦ Ordinal.iSup_le fun a ↦ ?_⟩
    rw [succ_le_iff]
    exact h (Mem.mk A a)

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