minimal_nonempty_open_eq_singleton

English

For a T0 space with a basis b, x=y iff for all s∈b, x∈s ⇔ y∈s.

Русский

Для T0-пространства с базисом b, x=y тогда и только тогда, когда для всех s∈b верно x∈s ⇔ y∈s.

LaTeX

$$$x=y \iff \forall s \in b, x\in s \iff y\in s.$$$

Lean4

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

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