isAtom_singleton

Mathlib.Order.Atoms

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

English

Singleton sets are atoms in the lattice of subsets.

Русский

Единственные множества являются атомами в решётке подмножеств.

LaTeX

$$$ IsAtom\left(\{x\}\right) $$$

Lean4

theorem isAtom_singleton (x : α) : IsAtom ({ x } : Set α) :=
  ⟨singleton_ne_empty _, fun _ hs => ssubset_singleton_iff.mp hs⟩

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

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

Разделы

Аффилиация

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