isCoatom_singleton_compl

Mathlib.Order.Atoms

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

English

For every x in α, the complement of the singleton {x} is a coatom of the power set of α.

Русский

Для каждого x ∈ α дополнение множества {x} является катомом булевой алгебры подмножеств α.

LaTeX

$$$\\mathrm{IsCoatom}({x}^{c})$$$

Lean4

theorem isCoatom_singleton_compl (x : α) : IsCoatom ({ x }ᶜ : Set α) :=
  (isCoatom_iff { x }ᶜ).mpr ⟨x, rfl⟩

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

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

Разделы

Аффилиация

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