exists_open_singleton_of_finite — Mathlib

English

In a finite, nonempty T0 space, there exists at least one open singleton {x}.

Русский

В конечном непустом T0-пространстве существует по меньшей мере одно открытое множество вида {x}.

LaTeX

$$$[T0Space X] \land [Finite X] \land [Nonempty X] \Rightarrow \exists x: X, IsOpen({x}).$$$

Lean4

theorem exists_open_singleton_of_finite [T0Space X] [Finite X] [Nonempty X] : ∃ x : X, IsOpen ({ x } : Set X) :=
  let ⟨x, _, h⟩ := exists_isOpen_singleton_of_isOpen_finite (Set.toFinite _) univ_nonempty isOpen_univ
  ⟨x, h⟩

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