English
If every f(i) ≥ 1 on s, then the product of any two elements is ≤ the product over s: f(i) f(j) ≤ ∏_{k∈s} f(k).
Русский
Если для всех i ∈ s верно f(i) ≥ 1, то произведение двух элементов не превосходит полного произведения: f(i) f(j) ≤ ∏_{k∈s} f(k).
LaTeX
$$$ \\forall \\iota\\, N\\, [\\text{CommMonoid } N], [\\text{PartialOrder } N], {f : \\iota \\to N} {s : \\mathrm{Finset} \\iota} [\\text{MulLeftMono } N], \\forall i\\in s, \\forall j\\in s, i\\neq j \\\\ → \\\\ f(i) \\cdot f(j) \\le \\prod_{k\\in s} f(k). $$$
Lean4
@[to_additive]
theorem mul_le_prod [MulLeftMono N] {i j : ι} (hf : ∀ i ∈ s, 1 ≤ f i) (hi : i ∈ s) (hj : j ∈ s) (hne : i ≠ j) :
f i * f j ≤ ∏ k ∈ s, f k :=
calc
f i * f j = ∏ k ∈ .cons i { j } (by simpa), f k := by rw [prod_cons, prod_singleton]
_ ≤ ∏ k ∈ s, f k := by
refine prod_le_prod_of_subset_of_one_le' ?_ fun k hk _ ↦ hf k hk
simp [cons_subset, *]
