monovaryOn_iff_mul_rearrangement — Mathlib

English

MonovaryOn f g s holds iff for all i ∈ s and j ∈ s, f i • g j + f j • g i ≤ f i • g i + f j • g j.

Русский

MonovaryOn f g s выполняется тогда и только тогда, когда для всех i ∈ s и j ∈ s верно 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 monovaryOn_iff_mul_rearrangement :
    MonovaryOn f g s ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → f i * g j + f j * g i ≤ f i * g i + f j * g j := by
  simp only [smul_eq_mul, monovaryOn_iff_smul_rearrangement]

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