isOpenEmbedding_iff_comp_isIso' — Mathlib

English

If f and g are morphisms with IsIso g, then IsOpenEmbedding (g ∘ f) is equivalent to IsOpenEmbedding f.

Русский

Если f и g — морфизмы и g — изоморфизм, тогда IsOpenEmbedding (g ∘ f) эквивалентно IsOpenEmbedding f.

LaTeX

$$$\\mathrm{IsOpenEmbedding}(g \\circ f) \\iff \\mathrm{IsOpenEmbedding}(f)$, при $IsIso(g)$$$

Lean4

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

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