monovary_iff_smul_rearrangement — Mathlib

English

Two functions monovary f and g on the universal set satisfy: for all i, j, f i • g j + f j • g i ≤ f i • g i + f j • g j.

Русский

Две функции моно-варьируют друг друга на всём множестве: для любых i, j выполняется f(i) • g(j) + f(j) • g(i) ≤ f(i) • g(i) + f(j) • g(j).

LaTeX

$$$MonovaryOn f g s \\iff \\forall i \\in s, \\forall j \\in s, f i \\bullet g j + f j \\bullet g i ≤ f i \\bullet g i + f j \\bullet g j$$$

Lean4

/-- Two functions monovary iff the rearrangement inequality holds. -/
theorem monovary_iff_smul_rearrangement : Monovary f g ↔ ∀ i j, f i • g j + f j • g i ≤ f i • g i + f j • g j :=
  monovaryOn_univ.symm.trans <| monovaryOn_iff_smul_rearrangement.trans <| by simp only [Set.mem_univ, forall_true_left]

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