map_op_nhds — Mathlib

English

The image of nhds under the operation map op coincides with the nhds of op x.

Русский

Изображение окрестностей под отображением op совпадает с окрестностями op x.

LaTeX

$$$$ \operatorname{map}(\mathrm{op}, \mathcal{N}(x)) = \mathcal{N}(\mathrm{op}(x)) $$$$

Lean4

@[to_additive (attr := simp)]
theorem map_op_nhds (x : M) : map (op : M → Mᵐᵒᵖ) (𝓝 x) = 𝓝 (op x) :=
  opHomeomorph.map_nhds_eq x

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