instRespectsIsoSchemeTopologicallyGeneralizingMap

English

An instance asserts that topologically generalized maps respect isomorphisms.

Русский

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

LaTeX

$$$\\text{(topologically GeneralizingMap).RespectsIso}$$$

Lean4

instance : (topologically GeneralizingMap).RespectsIso :=
  topologically_respectsIso _
    (fun f ↦ f.isOpenEmbedding.generalizingMap f.isOpenEmbedding.isOpen_range.stableUnderGeneralization)
    (fun _ _ hf hg ↦ hf.comp hg)

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