isCoatom_compl_singleton

Mathlib.Data.Finset.Grade

URI: https://scilib.ai/kg/mathlib#Finset.isCoatom_compl_singleton

English

The complement of a singleton is a coatom.

Русский

Дополнение одиночного множества образует коатом.

LaTeX

$$$ \text{IsCoatom}({a}^c) $$$

Lean4

theorem isCoatom_compl_singleton (a : α) : IsCoatom ({ a }ᶜ : Finset α) :=
  (isAtom_singleton a).compl

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

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

Разделы

Аффилиация

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