counit_comp_inr — Mathlib

English

Let A,B be coalgebras over R. The counit on the inr inclusion from B into A × B is the same as the counit on B; i.e. counit ∘ inr = counit.

Русский

Пусть A,B — коалгебры над R. Коунит на включении inr: B → A × B равен коуниту B; то есть counit ∘ inr = counit.

LaTeX

$$$ \operatorname{counit} \circ \mathrm{inr}_{R,A,B} = \operatorname{counit} $$$

Lean4

@[simp]
theorem counit_comp_inr : counit ∘ₗ inr R A B = counit := by ext; simp

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