antivaryOn_iff_forall_smul_nonpos

English

The monovary relation between f and g is equivalent to a universal nonnegativity condition on all pairs i,j in the domain.

Русский

Моновариантность между f и g эквивалентна всеобщему неотрицательному условию для всех пар i,j из области определения.

LaTeX

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

Lean4

theorem antivaryOn_iff_forall_smul_nonpos :
    AntivaryOn f g s ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0 :=
  monovaryOn_toDual_right.symm.trans <| by rw [monovaryOn_iff_forall_smul_nonneg]; rfl

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