dotProduct_le_dotProduct_of_nonneg_right

English

If u ≤ v componentwise and w ≥ 0 componentwise, then u · w ≤ v · w.

Русский

Если u ≤ v по каждому компоненту и w ≥ 0 по каждому компоненту, то u·w ≤ v·w.

LaTeX

$$u ≤ v \text{ and } 0 ≤ w \Rightarrow u \cdot w ≤ v \cdot w$$

Lean4

theorem dotProduct_le_dotProduct_of_nonneg_right {u v w : n → R} (huv : u ≤ v) (hw : 0 ≤ w) : u ⬝ᵥ w ≤ v ⬝ᵥ w :=
  Finset.sum_le_sum fun i _ => mul_le_mul_of_nonneg_right (huv i) (hw i)

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