mem_vonNeumann_of_subset

Mathlib.SetTheory.ZFC.VonNeumann

URI: https://scilib.ai/kg/mathlib#ZFSet.mem_vonNeumann_of_subset

← MathLib Explorer

English

If x ⊆ y and y ∈ V_o then x ∈ V_o.

Русский

Если x ⊆ y и y ∈ V_o, то x ∈ V_o.

LaTeX

$$$ x \subseteq y \land y \in V_o \Rightarrow x \in V_o $$$

Lean4

theorem mem_vonNeumann_of_subset {y : ZFSet} (h : x ⊆ y) (hy : y ∈ V_ o) : x ∈ V_ o :=
  by
  rw [mem_vonNeumann] at *
  exact (rank_mono h).trans_lt hy

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru