nhdsWithin_eq_map_subtype_coe — Mathlib

English

Within a subtype, the neighborhood of a point is the image under the inclusion map of the neighborhood of the corresponding point in the ambient space.

Русский

Внутри подтипа окрестность точки равна образу вложения от окрестности соответствующей точки в окружающем пространстве.

LaTeX

$$$ 𝓝[s] a = map (↑ : s \to α) (𝓝 ⟨a, h\rangle) $$$

Lean4

theorem nhdsWithin_eq_map_subtype_coe {s : Set α} {a : α} (h : a ∈ s) : 𝓝[s] a = map ((↑) : s → α) (𝓝 ⟨a, h⟩) :=
  (map_nhds_subtype_val ⟨a, h⟩).symm

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