nnnorm_smulRight_apply — Mathlib

English

The nonnegative norm (NNReal norm) of smulRight equals the product of the nonnegative norms: ||smulRight c f||_+ = ||c||_+ · ||f||_+.

Русский

Нормa противолежащей (NNReal) нормы для smulRight равняется произведению неотрицательных норм: ||smulRight c f||_+ = ||c||_+ · ||f||_+.

LaTeX

$$$ \\|smulRight\,c\,f\\|_+ = \\|c\\|_+ \\cdot \\|f\\|_+ $$$

Lean4

/-- The non-negative norm of the tensor product of a scalar linear map and of an element of a normed
space is the product of the non-negative norms. -/
@[simp]
theorem nnnorm_smulRight_apply (c : StrongDual 𝕜 E) (f : Fₗ) : ‖smulRight c f‖₊ = ‖c‖₊ * ‖f‖₊ :=
  NNReal.eq <| c.norm_smulRight_apply f

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