monovary_iff_mul_rearrangement — Mathlib

English

Monovary f g is equivalent to the rearrangement inequality with global indices: for all i, j, f i • g j + f j • g i ≤ f i • g i + f j • g j.

Русский

Моновариантность f и g эквивалентна глобальному перестановочному неравенству: для любых i, j выполняется f i • g j + f j • g i ≤ f i • g i + f j • g j.

LaTeX

$$$Monovary f g \\iff ∀ i j, 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_mul_rearrangement : Monovary f g ↔ ∀ i j, f i * g j + f j * g i ≤ f i * g i + f j * g j := by
  simp only [smul_eq_mul, monovary_iff_smul_rearrangement]

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