isAtom_iff

Mathlib.Data.Finset.Grade

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

English

A Finset s is an atom if and only if s is a singleton.

Русский

Финсет s является атомом тогда и только тогда, когда s является одиночным множеством.

LaTeX

$$$ \text{IsAtom}(s) \iff \exists a, s = \{a\} $$$

Lean4

protected theorem isAtom_iff : IsAtom s ↔ ∃ a, s = { a } := by simp [← bot_covBy_iff, covBy_iff_exists_cons, eq_comm]

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

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

Разделы

Аффилиация

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