English
If U is a neighborhood of every point of s, then there exists an open set V with s ⊆ V ⊆ U.
Русский
Если U является окрестностью каждого элемента множества s, то существует открытое множество V с s ⊆ V ⊆ U.
LaTeX
$$$\\forall s,U,\\ (\\forall x \\in s,\\ U \\in \\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 : ∀ x ∈ s, U ∈ 𝓝 x) : ∃ V : Set X, s ⊆ V ∧ IsOpen V ∧ V ⊆ U :=
⟨interior U, fun x hx => mem_interior_iff_mem_nhds.2 <| h x hx, isOpen_interior, interior_subset⟩
