id_comp

Mathlib.Topology.Order.Hom.Esakia

URI: https://scilib.ai/kg/mathlib#EsakiaHom.id_comp

English

Id composition on the left: (id β).comp f = f.

Русский

Левая тождественная композиция: (id β) .comp f = f.

LaTeX

$$$(\\text{EsakiaHom.id }\\beta).comp f = f$$$

Lean4

@[simp]
theorem id_comp (f : EsakiaHom α β) : (EsakiaHom.id β).comp f = f :=
  ext fun _ => rfl

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

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

Разделы

Аффилиация

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