monovary_iff_forall_mul_nonneg — Mathlib

English

Monovary f g is equivalent to the nonnegativity of the product (f j − f i) • (g j − g i) for all i, j.

Русский

Monovary f g эквивалентно неотрицательности произведения (f j − f i) • (g j − g i) для любых i, j.

LaTeX

$$$Monovary f g \\iff \\forall i j, 0 ≤ (f j - f i) \\bullet (g j - g i)$$$

Lean4

theorem monovary_iff_forall_mul_nonneg : Monovary f g ↔ ∀ i j, 0 ≤ (f j - f i) * (g j - g i) := by
  simp only [smul_eq_mul, monovary_iff_forall_smul_nonneg]

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