of_exists_mem_nhds_isClosed_subset

English

Let X be a topological space. If for every x ∈ X and every neighborhood s of x there exists a neighborhood t of x such that t is closed and t ⊆ s, then X is a regular space.

Русский

Пусть X — топологическое пространство. Если для каждой точки x ∈ X и любой окрестности s(x) существует окрестность t(x) такая, что t закрыто и t ⊆ s, то X является регулярным пространством.

LaTeX

$$$\forall x:\,x\in X \to \forall s:\,s \in \mathcal N(x) \;\exists t:\,t \in \mathcal N(x) \land \mathrm{IsClosed}(t) \land t \subseteq s \Rightarrow RegularSpace(X)$$$

Lean4

theorem of_exists_mem_nhds_isClosed_subset (h : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s) : RegularSpace X :=
  Iff.mpr ((regularSpace_TFAE X).out 0 3) h

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