exists_mem_nhds_isClosed_subset — Mathlib

English

If s is a neighborhood of x, there exists a closed neighborhood t of x such that t ⊆ s.

Русский

Если s — окрестность x, существует замкнутая окрестность t x такая, что t ⊆ s.

LaTeX

$$$\forall x:\, x\in X,\forall s:\, s\in 𝓝 x \Rightarrow\exists t:\, t\in 𝓝 x \land IsClosed(t) \land t\subseteq s$$$

Lean4

theorem exists_mem_nhds_isClosed_subset {x : X} {s : Set X} (h : s ∈ 𝓝 x) : ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s :=
  by
  have h' := (regularSpace_TFAE X).out 0 3
  exact h'.mp ‹_› _ _ h

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