monovaryOn_iff_forall_mul_nonneg — Mathlib

English

Two functions are monovary if and only if for all i, j one has 0 ≤ (f j − f i) • (g j − g i).

Русский

Две функции моновариантны тогда и только тогда, когда для любых i, j верно 0 ≤ (f j − f i) • (g j − g i).

LaTeX

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

Lean4

theorem monovaryOn_iff_forall_mul_nonneg :
    MonovaryOn f g s ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → 0 ≤ (f j - f i) * (g j - g i) := by
  simp only [smul_eq_mul, monovaryOn_iff_forall_smul_nonneg]

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