isTransitive_vonNeumann — Mathlib

English

For every ordinal o, V_o is transitive; i.e., if a ∈ b and b ∈ V_o then a ∈ V_o.

Русский

Для каждого ординала o множество V_o транзитивно; если a ∈ b ∈ V_o, то a ∈ V_o.

LaTeX

$$$$ \text{For all } o,\; V_{o}.IsTransitive $$$$

Lean4

theorem isTransitive_vonNeumann (o : Ordinal) : IsTransitive (V_ o) :=
  by
  rw [vonNeumann]
  refine IsTransitive.sUnion' fun x hx ↦ ?_
  obtain ⟨⟨a, _⟩, rfl⟩ := mem_range.1 hx
  exact (isTransitive_vonNeumann a).powerset
termination_by o

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