isAtom_iff — Mathlib

English

In a T1 space, IsAtom (s as a set) is equivalent to IsAtom s as a closed set.

Русский

В пространстве T1, IsAtom (s как множество) эквивалентно IsAtom s как замкнутое множество.

LaTeX

$$$ IsAtom((s : Set\\,\\alpha)) \\iff IsAtom(s). $$$

Lean4

/-- in a `T1Space`, atoms of `TopologicalSpace.Closeds α` are precisely the
`TopologicalSpace.Closeds.singleton`s. -/
theorem isAtom_iff [T1Space α] {s : Closeds α} : IsAtom s ↔ ∃ x, s = Closeds.singleton x := by
  simp [← Closeds.isAtom_coe, Set.isAtom_iff, SetLike.ext_iff, Set.ext_iff]

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