nhds_eq_map_structureMap — Mathlib

English

The nhds of the structure map equals the map of nhds; the point follows from open embedding property.

Русский

Окрестности карты структуры равны отображению окрестностей; следует из открытого вложения.

LaTeX

$$$\\mathcal{nhds}(\\text{structureMap } R A\\, x) = \\mathrm{map}(\\text{structureMap } R A)(\\mathcal{nhds}(x))$$$

Lean4

theorem nhds_eq_map_structureMap (x : Π i, A i) :
    (𝓝 (structureMap R A cofinite x)) = .map (structureMap R A cofinite) (𝓝 x) := by
  rw [isOpenEmbedding_structureMap hAopen |>.map_nhds_eq x]

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