isIso_of_isIso_left_of_isIso_right

English

If both components of a morphism of arrows are isomorphisms, then the morphism of arrows is an isomorphism.

Русский

Если обе компоненты морфизма стрел изоморфизмы, то сам морфизм стрел является изоморфизмом.

LaTeX

$$$IsIso(ff.left) \land IsIso(ff.right) \Rightarrow IsIso(ff)$$$

Lean4

theorem isIso_of_isIso_left_of_isIso_right {f g : Arrow T} (ff : f ⟶ g) [IsIso ff.left] [IsIso ff.right] : IsIso ff
    where
  out := by
    let inverse : g ⟶ f := ⟨inv ff.left, inv ff.right, (by simp)⟩
    apply Exists.intro inverse
    cat_disch

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