norm_const_le — Mathlib

English

The norm of a constant function is at most the norm of its value (repeated statement of norm_const_le).

Русский

Норма константной функции не превосходит нормы её значения.

LaTeX

$$$\\|const\\;\\alpha b\\| \\le \\|b\\|$$$

Lean4

/-- Norm of `const α b` is less than or equal to `‖b‖`. If `α` is nonempty,
then it is equal to `‖b‖`. -/
theorem norm_const_le (b : β) : ‖const α b‖ ≤ ‖b‖ :=
  (norm_le (norm_nonneg b)).2 fun _ => le_rfl

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