counit_comp_apply — Mathlib

English

The counit is natural with respect to the coercion f: F → A → B; applying counit after f equals applying counit on x directly.

Русский

Коуни́т сохраняет естественность при отношении к отображению f: F → A → B; применение коуни́та после f равно применению коуни́та к x.

LaTeX

$$$\\text{counit}(f x) = \\text{counit}(x)$$$

Lean4

@[simp]
theorem counit_comp_apply (f : F) (x : A) : counit (f x) = counit (R := R) x :=
  LinearMap.congr_fun (counit_comp f) _

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