instCoalgebraStruct — Mathlib

English

The counit composed with the inr injection from B into A × B is equal to the counit on B; this equality holds by simplifications.

Русский

Коунит, композиция с инр-вставкой из B в A × B, равен коуниту B; равенство следует из упрощений.

LaTeX

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

Lean4

instance instCoalgebraStruct : CoalgebraStruct R (Π₀ i, A i)
    where
  comul := DFinsupp.lsum R fun i => TensorProduct.map (DFinsupp.lsingle i) (DFinsupp.lsingle i) ∘ₗ comul
  counit := DFinsupp.lsum R fun _ => counit

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