toContinuousAddMonoidHom_comp — Mathlib

English

The function coercion of a composition equals the composition of coerced functions: (h ∘ f)^{coerced} = h^{coerced} ∘ f^{coerced}.

Русский

Приведение составной функции к функциям-частям эквивалентно композиции приведённых функций: (h ∘ f)^{coerced} = h^{coerced} ∘ f^{coerced}.

LaTeX

$$$ (h \\circ f) = h \\circ f $ under the appropriate coercions.$$

Lean4

@[simp, norm_cast]
theorem toContinuousAddMonoidHom_comp (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
    (↑(h.comp f) : ContinuousAddMonoidHom M₁ M₃) = (h : ContinuousAddMonoidHom M₂ M₃).comp f :=
  rfl

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