nhds_subtype_eq_comap_nhdsWithin — Mathlib

English

For any subset s ⊆ X and x ∈ {x ∈ s}, the neighborhood 𝓝 x in the subtype equals comap of the inclusion with nhdsWithin x in X, restricted to s.

Русский

Для подмножества s ⊆ X и x ∈ {x ∈ s}, окрестность 𝓝 x в подтипе равна comap включения к nhdsWithin x в X на s.

LaTeX

$$$ 𝓝 x = \\operatorname{comap}(\\mathrm{Subtype}.val)(𝓝[s](x.1)). $$$

Lean4

theorem nhds_subtype_eq_comap_nhdsWithin (s : Set X) (x : { x // x ∈ s }) : 𝓝 x = comap (↑) (𝓝[s] (x : X)) := by
  rw [nhds_subtype, ← comap_nhdsWithin_range, Subtype.range_val]

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