coe_comp — Mathlib

English

Coercion respects composition: the coercion of a composition equals the composition of coercions.

Русский

Приведение сохраняет композицию: привод f ∘ g равно приведениям f и g по отдельности.

LaTeX

$$$(g\\circ f)^{\\;toContinuousMonoidHom} = g^{toContinuousMonoidHom} \\circ f^{toContinuousMonoidHom}$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_comp (g : ContinuousMonoidHom B C) (f : ContinuousMonoidHom A B) : ⇑(g.comp f) = ⇑g ∘ ⇑f :=
  rfl

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