cancel_counit_right — Mathlib

English

In an equivalence e, postcomposition with the counit at Y is injective on morphisms with domain X and codomain e.functor.obj (e.inverse.obj Y).

Русский

В эквивалентности e посткомпозиция по counit в Y инъективна на морфизмах с началом X и концом e.functor.obj (e.inverse.obj Y).

LaTeX

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

Lean4

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

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