isCoatom_iff

Mathlib.Data.Finset.Grade

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

← MathLib Explorer

English

A Finset s is a coatom iff its complement is a singleton.

Русский

Финсет s является коатомом тогда и только тогда, когда его дополнение — одиночный набор.

LaTeX

$$$ \text{IsCoatom}(s) \iff \exists a, s = {a}^c $$$

Lean4

protected theorem isCoatom_iff : IsCoatom s ↔ ∃ a, s = { a }ᶜ := by
  simp_rw [← isAtom_compl, Finset.isAtom_iff, compl_eq_iff_isCompl, eq_compl_iff_isCompl]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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