isAtom_singleton

Mathlib.Data.Finset.Grade

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

English

A Finset consisting of a single element is an atom in the Finset lattice.

Русский

Финсет, состоящий из одного элемента, является атомом в решетке Finset.

LaTeX

$$$ \text{IsAtom}({a}) $$$

Lean4

@[simp]
theorem isAtom_singleton (a : α) : IsAtom ({ a } : Finset α) :=
  ⟨singleton_ne_empty a, fun _ ↦ eq_empty_of_ssubset_singleton⟩

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

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

Разделы

Аффилиация

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