enorm_apply_le — Mathlib

English

Let p ≥ 1 and ι be finite. For any x in the Lp-product PiLp p β, the i-th coordinate satisfies the bound ||x_i|| ≤ ||x||_p for every i ∈ ι.

Русский

Пусть p ≥ 1 и ι — конечно множество. Для любого x в пространстве PiLp p β выполняется неравенство ||x_i|| ≤ ||x||_p для каждого i ∈ ι.

LaTeX

$$$$ \forall i : \iota,\; \|x_i\| \le \|x\|_p $$$$

Lean4

theorem enorm_apply_le [∀ i, SeminormedAddCommGroup (β i)] (x : PiLp p β) (i : ι) : ‖x i‖ₑ ≤ ‖x‖ₑ := by
  simpa using edist_apply_le x 0 i

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