isCoatom_iff — Mathlib

English

In the lattice of subsets of α (ordered by inclusion), a subset s is a coatom if and only if it is the complement of a singleton, i.e., s = {x}^c for some x.

Русский

В решётке подмножеств α по включению элемент s является катомом тогда, когда он является дополнением к одиночному множеству: s = {x}^c для некоторого x.

LaTeX

$$$\\mathrm{IsCoatom}(s) \\iff \\exists x, s = {x}^{c}$$$

Lean4

theorem isCoatom_iff (s : Set α) : IsCoatom s ↔ ∃ x, s = { x }ᶜ :=
  by
  rw [isCompl_compl.isCoatom_iff_isAtom, isAtom_iff]
  simp_rw [@eq_comm _ s, compl_eq_comm]

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