exists_open_set_nhds' — Mathlib

English

If U is a neighborhood of every point of s (in the sense of iSup over s), then there exists an open V with s ⊆ V ⊆ U.

Русский

Если U является окрестностью каждого элемента s в смысле iSup над s, то существует открытое V с s ⊆ V ⊆ U.

LaTeX

$$$\\forall s,U,\\ (U \\in \\bigsqcup_{x \\in s} \\mathcal N_x) \\Rightarrow \\exists V,\\ s \\subseteq V \\land IsOpen(V) \\land V \\subseteq U.$$$

Lean4

/-- If `U` is a neighborhood of each point of a set `s` then it is a neighborhood of s:
it contains an open set containing `s`. -/
theorem exists_open_set_nhds' {U : Set X} (h : U ∈ ⨆ x ∈ s, 𝓝 x) : ∃ V : Set X, s ⊆ V ∧ IsOpen V ∧ V ⊆ U :=
  exists_open_set_nhds (by simpa using h)

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