norm_le_pi_norm'

Mathlib.Analysis.Normed.Group.Constructions

URI: https://scilib.ai/kg/mathlib#norm_le_pi_norm'

English

For any i, the norm of the i-th component is bounded by the norm of the whole tuple: ∥f(i)∥ ≤ ∥f∥.

Русский

Для любого i нормa i-й компоненты не превышает норму всего кортежа: ∥f(i)∥ ≤ ∥f∥.

LaTeX

$$$\|f(i)\| \le \|f\|$$$

Lean4

@[to_additive norm_le_pi_norm]
theorem norm_le_pi_norm' (i : ι) : ‖f i‖ ≤ ‖f‖ :=
  (pi_norm_le_iff_of_nonneg' <| norm_nonneg' _).1 le_rfl i

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru