isOpenEmbedding_structureMap — Mathlib

English

The nhds of the structure map matches the map of nhds, i.e., the neighborhood filter commutes with the structure map.

Русский

Окрестности карты структуры совпадают с отображением окрестностей: фильтр окрестностей синхронизируется с картой структуры.

LaTeX

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

Lean4

/-- `Π i, A i` is homeomorphic to an open subset of the restricted product. -/
theorem isOpenEmbedding_structureMap : IsOpenEmbedding (structureMap R A cofinite)
    where
  toIsEmbedding := isEmbedding_structureMap
  isOpen_range := by
    rw [range_structureMap]
    exact isOpen_forall_mem hAopen

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