cancel_counitInv_right — Mathlib

English

The counitInv is cancellative on the right: postcomposition with counitInv at Y is injective on morphisms.

Русский

Обратная единица counitInv слева совместимо с отменой на правой стороне: посткомпозиция с counitInv в Y инъективна.

LaTeX

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

Lean4

@[simp]
theorem cancel_counitInv_right {X Y : D} (f f' : X ⟶ Y) : f ≫ e.counitInv.app Y = f' ≫ e.counitInv.app Y ↔ f = f' := by
  simp only [cancel_mono]

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