English
In a T1 space, coatoms of Opens α are exactly the complements of singleton closures: IsCoatom s iff there exists x with s = (Closeds.singleton x).compl.
Русский
В пространстве T1 коатомы открытых равны complemento одиночного замкнутого множества: IsCoatom s ⇔ ∃ x, s = (Closeds.singleton x).compl.
LaTeX
$$$ IsCoatom(s) \\iff \\exists x, s = (Closeds.singleton(x)).compl. $$$
Lean4
/-- in a `T1Space`, coatoms of `TopologicalSpace.Opens α` are precisely complements of singletons:
`(TopologicalSpace.Closeds.singleton x).compl`. -/
theorem isCoatom_iff [T1Space α] {s : Opens α} : IsCoatom s ↔ ∃ x, s = (Closeds.singleton x).compl :=
by
rw [← s.compl_compl, ← isAtom_dual_iff_isCoatom]
change IsAtom (Closeds.complOrderIso α s.compl) ↔ _
simp only [(Closeds.complOrderIso α).isAtom_iff, Closeds.isAtom_iff, Closeds.compl_bijective.injective.eq_iff]
