id_apply

Mathlib.Algebra.Category.CommBialgCat

URI: https://scilib.ai/kg/mathlib#CommBialgCat.id_apply

English

The identity morphism acts as the identity on all elements of the carrier.

Русский

Тождественный морфизм действует как тождественный отображение на каждом элементе носителя.

LaTeX

$$$ (\mathrm{id}_A)(a) = a $$$

Lean4

theorem id_apply (A : CommBialgCat.{v} R) (a : A) : (𝟙 A : A ⟶ A) a = a := by simp

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

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

Разделы

Аффилиация

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