cancel_unitInv_right — Mathlib

English

Symmetric statement to the previous one, for the unit inverse: postcomposition with the unitInv at Y is also cancellative on morphisms.

Русский

Аналогично предыдущему, но для обратной единицы: посткомпозиция с unitInv в Y также обеспечивает отмену на морфизмах.

LaTeX

$$$\forall X,Y\ (f,f' : X \to e.inverse.obj (e.functor.obj Y)),\; f \;\xrightarrow{\mathrm{unitInv}.app Y} = f' \;\xrightarrow{\mathrm{unitInv}.app Y} \Rightarrow f=f'$$$

Lean4

@[simp]
theorem cancel_unitInv_right {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) :
    f ≫ e.unitInv.app Y = f' ≫ e.unitInv.app Y ↔ f = f' := by simp only [cancel_mono]

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