single_le_finprod — Mathlib

English

If the support of f is finite and f(i) ≥ 1 for all i, then f(i) ≤ ∏ᶠ j, f(j) for any i.

Русский

Если опора f конечна и f(i) ≥ 1, то f(i) ≤ произведение по всем j.

LaTeX

$$$f(i) \\le \\prod^\\!j, f(j)$$$

Lean4

@[to_additive]
theorem single_le_finprod {M : Type*} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] (i : α) {f : α → M}
    (hf : (mulSupport f).Finite) (h : ∀ j, 1 ≤ f j) : f i ≤ ∏ᶠ j, f j := by
  classical
    calc
    f i ≤ ∏ j ∈ insert i hf.toFinset, f j := Finset.single_le_prod' (fun j _ => h j) (Finset.mem_insert_self _ _)
    _ = ∏ᶠ j, f j := (finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_insert _ _)).symm

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