mem_compl_singleton_iff

Mathlib.Order.BooleanAlgebra.Set

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

English

Membership in the complement of a singleton is equivalent to inequality.

Русский

Членство в дополнении одиночного множества эквивалентно неравенству.

LaTeX

$$$a \in ({b} : Set \alpha)^{c} \iff a \neq b$$$

Lean4

theorem mem_compl_singleton_iff : a ∈ ({ b } : Set α)ᶜ ↔ a ≠ b :=
  .rfl

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

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

Разделы

Аффилиация

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