English
Neighborhoods in the quotient G/N correspond exactly to the images under the quotient map of neighborhoods in G: for all x ∈ G, nhds of the coset xN equals the pushforward of nhds(x).
Русский
Окрестности в фактор-пространстве G/N соответствуют образам окрестностей в G через отображение факторизации: для всех x ∈ G, окрестность coset xN равна образу окрестности x.
LaTeX
$$$\mathcal{N}_{G/N}(\widehat{x}) = \operatorname{map}(\iota)(\mathcal{N}_{G}(x)).$$$
Lean4
/-- Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient. -/
@[to_additive /-- Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient. -/
]
theorem nhds_eq (x : G) : 𝓝 (x : G ⧸ N) = Filter.map (↑) (𝓝 x) :=
(isOpenQuotientMap_mk.map_nhds_eq _).symm
