specializingMap_respectsIso — Mathlib

English

The specialization map, viewed topologically, respects isomorphisms.

Русский

Специализирующая карта, рассматриваемая в топологическом виде, сохраняется при изоморфизмах.

LaTeX

$$$\\mathrm{RespectsIso} (\\text{topologically } \\mathrm{SpecializingMap})$$$

Lean4

instance specializingMap_respectsIso : (topologically @SpecializingMap).RespectsIso :=
  by
  apply topologically_respectsIso
  · introv
    exact f.isClosedMap.specializingMap
  · introv hf hg
    exact hf.comp hg

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