vonNeumann_of_isSuccPrelimit — Mathlib

English

If o is IsSuccPrelimit, then V_o equals the union over a ∈ Iio(o) of vonNeumann a.

Русский

Если o является IsSuccPrelimit, то V_o равно объединению по a ∈ Iio(o) vonNeumann a.

LaTeX

$$$ V_o = \bigcup_{a \in \mathrm{Iio}(o)} V_a $$$

Lean4

theorem vonNeumann_of_isSuccPrelimit (h : IsSuccPrelimit o) :
    V_ o = (⋃₀ range fun a : Set.Iio o ↦ vonNeumann a : ZFSet) :=
  ext fun z ↦ by simpa [mem_vonNeumann] using h.lt_iff_exists_lt

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