map_inr_inv_coprodComparison — Mathlib

English

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

Русский

Если coprodComparison F A B изоморфизм, то F.map coprod.inr ∘ inv (coprodComparison F A B) = coprod.inr.

LaTeX

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

Lean4

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

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