toContinuousAddMonoidHom_neg — Mathlib

English

For any f, the negation -f, regarded as a ContinuousAddMonoidHom, corresponds to negation of f as a map.

Русский

Для любого f отрицание -f, как ContinuousAddMonoidHom, соответствует отрицанию f как отображения.

LaTeX

$$↑(-f) = -(f : ContinuousAddMonoidHom M M₂)$$

Lean4

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

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