toContinuousAddMonoidHom_add — Mathlib

English

The embedding of endomorphisms into a ContinuousAddMonoidHom respects addition: the image of f+g equals the sum of images.

Русский

Встраивание эндоморфизмов в ContinuousAddMonoidHom сохраняет сложение: образ f+g равен сумме образов.

LaTeX

$$$?\\,\\uparrow(f+g) = \\uparrow f + \\uparrow g$$$

Lean4

@[simp, norm_cast]
theorem toContinuousAddMonoidHom_add (f g : M₁ →SL[σ₁₂] M₂) : ↑(f + g) = (f + g : ContinuousAddMonoidHom M₁ M₂) :=
  rfl

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