of_nnnorm_smul — Mathlib

English

If there is a function h such that ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊ for all r,x, then NormSMulClass α β exists.

Русский

Если существует функция h, удовлетворяющая ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊ для всех r,x, то существует NormSMulClass α β.

LaTeX

$$$NormSMulClass\\;\\alpha\\;\\beta$$$

Lean4

theorem of_nnnorm_smul (h : ∀ (r : α) (x : β), ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊) : NormSMulClass α β where
  norm_smul r b := congr_arg NNReal.toReal (h r b)

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