singleton_inter_eq_empty

Mathlib.Data.Set.Insert

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

English

{a} ∩ s = ∅ ↔ a ∉ s

Русский

{a} ∩ s = ∅ ↔ a ∉ s

LaTeX

$$$\\{ a \\} \\cap s = \\emptyset \\iff a \\notin s$$$

Lean4

@[simp]
theorem singleton_inter_eq_empty : { a } ∩ s = ∅ ↔ a ∉ s :=
  not_nonempty_iff_eq_empty.symm.trans singleton_inter_nonempty.not

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

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

Разделы

Аффилиация

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