dotProduct_le_dotProduct_of_nonneg_left

Mathlib.LinearAlgebra.Matrix.DotProduct

URI: https://scilib.ai/kg/mathlib#dotProduct_le_dotProduct_of_nonneg_left

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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