nonempty_of_mem

Mathlib.SetTheory.ZFC.Basic

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

English

If x is an element of u, then u is nonempty.

Русский

Пусть x и u — элементы ZFSet; если x ∈ u, то u непусто.

LaTeX

$$$\forall x,u:\mathrm{ZFSet}, x \in u \Rightarrow u \neq \emptyset$$$

Lean4

theorem nonempty_of_mem {x u : ZFSet} (h : x ∈ u) : u.Nonempty :=
  ⟨x, h⟩

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

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

Разделы

Аффилиация

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