eq_empty

Mathlib.SetTheory.ZFC.Basic

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

English

A set x equals the empty set if and only if every element is not in x.

Русский

Множество x равно пустому тогда и только тогда, когда для любого y неверно, что y ∈ x.

LaTeX

$$$\forall x : ZFSet, x = \emptyset \iff \forall y : ZFSet, y \notin x$$$

Lean4

theorem eq_empty (x : ZFSet.{u}) : x = ∅ ↔ ∀ y : ZFSet.{u}, y ∉ x := by simp [ZFSet.ext_iff]

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

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

Разделы

Аффилиация

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