subset_vonNeumann — Mathlib

English

Let o be an ordinal and x a ZF set. Then x ⊆ V_o if and only if rank(x) ≤ o.

Русский

Пусть o — ординал, x — множество ЗФ. Тогда x ⊆ V_o тогда и только если rank(x) ≤ o.

LaTeX

$$$ x \subseteq V_o \iff \operatorname{rank}(x) \le o $$$

Lean4

theorem subset_vonNeumann {o : Ordinal} {x : ZFSet} : x ⊆ V_ o ↔ rank x ≤ o :=
  by
  rw [rank_le_iff]
  constructor <;> intro hx y hy
  · apply (rank_lt_of_mem (hx hy)).trans_le
    simp_rw [rank_le_iff, mem_vonNeumann']
    rintro z ⟨a, ha, hz⟩
    exact (subset_vonNeumann.1 hz).trans_lt ha
  · rw [mem_vonNeumann']
    have := hx hy
    exact ⟨_, this, subset_vonNeumann.2 le_rfl⟩
termination_by o

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