counit_comul

Mathlib.CategoryTheory.Bicategory.Monad.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Bicategory.Comonad.counit_comul

English

Comonad counit-comultiplication law: Δ ≫ ε ▷ t = λ_t^{-1}.

Русский

Закон комонета counit comul: Δ ≫ ε ▷ t = λ_t^{-1}.

LaTeX

$$$Δ \\;≫\\; ε \\triangleright t = (λ_ t)^{-1}$$$

Lean4

@[reassoc (attr := simp)]
theorem counit_comul : Δ ≫ ε ▷ t = (λ_ t).inv :=
  ComonObj.counit_comul t

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru