coe_eq_singleton_of_isAtom — Mathlib

English

If α is a T0 space and s is an atom in the lattice of closed sets of α, then s is a singleton: there exists a ∈ α with s = {a}.

Русский

Если α — пространство T0 и s — атом в решётке замкнутых множеств α, то s является синглтоном: существует a ∈ α такое что s = {a}.

LaTeX

$$$ [T0Space(\\alpha)]\\; IsAtom(s) \\Rightarrow \\Exists a, (s : Set\\,\\alpha) = \\{a\\}. $$$

Lean4

theorem coe_eq_singleton_of_isAtom [T0Space α] {s : Closeds α} (hs : IsAtom s) : ∃ a, (s : Set α) = { a } :=
  by
  refine minimal_nonempty_closed_eq_singleton s.2 (coe_nonempty.2 hs.1) fun t hts ht ht' ↦ ?_
  lift t to Closeds α using ht'
  exact SetLike.coe_injective.eq_iff.2 <| (hs.le_iff_eq <| coe_nonempty.1 ht).1 hts

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