comapEq_trans — Mathlib

English

For functions f,g,h: β → γ with k : f = g and l : g = h, comapEq C (k.trans l) equals the composition comapEq C k ≪≫ comapEq C l. This expresses compatibility of comapEq with function composition.

Русский

Для функций f,g,h: β → γ, при k : f = g и l : g = h, comapEq C (k.trans l) равен композиции comapEq C k и comapEq C l.

LaTeX

$$$ comapEq\, C\, (k\\,\\.trans\\, l) = comapEq\, C\, k \\;\\llcorner\\; comapEq\, C\, l $$$

Lean4

theorem comapEq_trans {β γ : Type w} {f g h : β → γ} (k : f = g) (l : g = h) :
    comapEq C (k.trans l) = comapEq C k ≪≫ comapEq C l := by cat_disch

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