isOpenEmbedding_iff_isIso_comp' — Mathlib

English

An equivalence of composition with an isomorphism preserves open embeddings.

Русский

Эквивалентность композиции с изоморфизмом сохраняет открытые вложения.

LaTeX

$$$\\mathrm{IsOpenEmbedding}((\\text{functor} \\_) \\circ (\\text{hom})) \\text{ is preserved under } IsIso$$

Lean4

@[simp]
theorem isOpenEmbedding_iff_isIso_comp' {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] :
    IsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding g := by
  simp only
  exact isOpenEmbedding_iff_isIso_comp f g

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