instRespectsIsoSchemeTopologicallyIsOpenEmbedding

English

The surjectivity/open-embedding properties respect isomorphisms in the underlying maps.

Русский

Свойства сюръективности/открытого вложения унаследованы из изоморфизмов в базисных отображениях.

LaTeX

$$$\mathrm{RespectsIso}(\text{Surjective})$$$

Lean4

instance : (topologically IsOpenEmbedding).RespectsIso :=
  topologically_respectsIso _ (fun e ↦ e.isOpenEmbedding) (fun _ _ hf hg ↦ hg.comp hf)

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