counit_comp_inl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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