interior_mem_nhds — Mathlib

English

For any X with a topology and any s ⊆ X, the property interior s ∈ 𝓝(x) is equivalent to s ∈ 𝓝(x) for all x; i.e., interior membership in nhds is equivalent to membership of the original set in nhds.

Русский

Для любого x в X и множества s ⊆ X верно: interior s ∈ 𝓝(x) эквивалентно s ∈ 𝓝(x).

LaTeX

$$$\\forall x, (\\operatorname{int}(s) \\in \\mathcal{N}(x)) \\iff (s \\in \\mathcal{N}(x))$$$

Lean4

@[simp]
theorem interior_mem_nhds : interior s ∈ 𝓝 x ↔ s ∈ 𝓝 x :=
  ⟨fun h => mem_of_superset h interior_subset, fun h => IsOpen.mem_nhds isOpen_interior (mem_interior_iff_mem_nhds.2 h)⟩

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