antivaryOn_iff_forall_mul_nonpos — Mathlib

English

Two functions antivary on a subset s if and only if for all i ∈ s and j ∈ s one has (f j − f i) • (g j − g i) ≤ 0.

Русский

Две функции antivary на подмножестве s эквивалентно условию: для любых i, j ∈ s выполняется (f j − f i) • (g j − g i) ≤ 0.

LaTeX

$$$AntivaryOn f g s \\iff \\forall i \\in s, \\forall j \\in s, (f j - f i) \\bullet (g j - g i) ≤ 0$$$

Lean4

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

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