monovary_iff_forall_smul_nonneg — Mathlib

English

The monovary property between two functions f and g is characterized by a single universal nonnegativity condition on all pairs of indices.

Русский

Свойство моновариантности между двумя функциями f и g характеризуется одним всеобщим неотрицательным условием для всех пар индексов.

LaTeX

$$$\\text{Monovary}(f,g) \\iff \\forall i,j,\\; 0 \\le (f(j)-f(i)) \\bullet (g(j)-g(i))$$$

Lean4

theorem monovary_iff_forall_smul_nonneg : Monovary f g ↔ ∀ i j, 0 ≤ (f j - f i) • (g j - g i) :=
  monovaryOn_univ.symm.trans <| monovaryOn_iff_forall_smul_nonneg.trans <| by simp only [Set.mem_univ, forall_true_left]

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