map_mk_nhdsWithin_preimage — Mathlib

English

For any subset s of SeparationQuotient X and any x ∈ X, the pushforward under mk of the nhdsWithin of x inside mk^{-1}(s) equals the nhdsWithin of mk x inside s.

Русский

Для множества s в SeparationQuotient X и точки x ∈ X образ mk отправляет окрестности внутри mk^{-1}(s) в окрестности внутри s точки mk x.

LaTeX

$$$\\mathrm{map}\\big(\\mathrm{mk}\\big)\\big(\\mathcal{N}_{\\mathrm{within}}(x; \\mathrm{mk}^{-1}(s))\\big) = \\mathcal{N}_{\\mathrm{within}}(\\mathrm{mk} x; s)$$$

Lean4

theorem map_mk_nhdsWithin_preimage (s : Set (SeparationQuotient X)) (x : X) : map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x := by
  rw [nhdsWithin, ← comap_principal, Filter.push_pull, nhdsWithin, map_mk_nhds]

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