inv_prodComparison_map_snd — Mathlib

English

If prodComparison F A B is an isomorphism, then inv(prodComparison F A B) ≫ F.map prod.fst = prod.fst.

Русский

Если prodComparison F A B является изоморфизмом, то inv(prodComparison F A B) ∘ F.map prod.fst = prod.fst.

LaTeX

$$$ inv(\\operatorname{prodComparison} F A B) \\circ F(\\operatorname{prod.fst}) = \\operatorname{prod.fst} $$$

Lean4

@[reassoc]
theorem inv_prodComparison_map_snd [IsIso (prodComparison F A B)] :
    inv (prodComparison F A B) ≫ F.map prod.snd = prod.snd := by simp [IsIso.inv_comp_eq]

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