minimal_nonempty_closed_eq_singleton

English

If a nonempty closed set s in a T0 space is minimal nonempty closed under inclusion, then s is a singleton.

Русский

Если непустое замкнутое множество s минимально по включению, то оно равно множеству-одиночке.

LaTeX

$$$\exists x, s = \{x\}$ under given hypotheses.$$

Lean4

theorem minimal_nonempty_closed_eq_singleton [T0Space X] {s : Set X} (hs : IsClosed s) (hne : s.Nonempty)
    (hmin : ∀ t, t ⊆ s → t.Nonempty → IsClosed t → t = s) : ∃ x, s = { x } :=
  exists_eq_singleton_iff_nonempty_subsingleton.2 ⟨hne, minimal_nonempty_closed_subsingleton hs hmin⟩

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