map_inl_inv_coprodComparison — Mathlib

English

If coprodComparison F A B is an isomorphism, then F.map coprod.inl ≫ inv (coprodComparison F A B) = coprod.inl.

Русский

Если coprodComparison F A B является изоморфизмом, то F.map coprod.inl ≫ inv (coprodComparison F A B) = coprod.inl.

LaTeX

$$$ F.map(\\mathrm{coprod.inl}) \\circ inv(\\mathrm{coprodComparison} F A B) = \\mathrm{coprod.inl} $$$

Lean4

@[reassoc]
theorem map_inl_inv_coprodComparison [IsIso (coprodComparison F A B)] :
    F.map coprod.inl ≫ inv (coprodComparison F A B) = coprod.inl := by simp

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