pi_norm_const_le' — Mathlib

English

The sup-norm of a constant function a ∈ E across all indices is bounded by the norm of a: ‖fun i => a‖ ≤ ‖a‖.

Русский

Супремальная норма константной функции a по всем индексам не превосходит норму a: \|fun i => a\| ≤ \|a\|.

LaTeX

$$$\|\mathrm{const}_a\| \le \|a\|$$$

Lean4

@[to_additive pi_norm_const_le]
theorem pi_norm_const_le' (a : E) : ‖fun _ : ι => a‖ ≤ ‖a‖ :=
  (pi_norm_le_iff_of_nonneg' <| norm_nonneg' _).2 fun _ => le_rfl

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