eq_empty_of_forall_notMem

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.eq_empty_of_forall_notMem

English

If every element is not in s, then s equals the empty set.

Русский

Если каждый элемент не принадлежит s, то s равно пустому множеству.

LaTeX

$$$$ (\forall x, x \notin s) \Rightarrow s = \emptyset. $$$$

Lean4

theorem eq_empty_of_forall_notMem (h : ∀ x, x ∉ s) : s = ∅ :=
  subset_empty_iff.1 h

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

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

Разделы

Аффилиация

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