left_hom_inv_right — Mathlib

English

For e: X ⟶ Y in the comma category with IsIso e, the composite L.map (inv e.left) ≫ X.hom ≫ R.map e.right equals Y.hom.

Русский

Для e: X ⟶ Y в комма‑категории с IsIso e композиция L.map (inv e.left) ≫ X.hom ≫ R.map (e.right) равна Y.hom.

LaTeX

$$$ L.map(\mathrm{inv}(e.left)) \; \circ X.hom \circ R.map(e.right) = Y.hom. $$$

Lean4

theorem left_hom_inv_right [IsIso e] : L.map (e.left) ≫ Y.hom ≫ R.map (inv e.right) = X.hom := by simp

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