single_le_prod' — Mathlib

English

If a ∈ s and f(a) ≤ ∏_{x∈s} f(x), then f(a) ≤ ∏_{x∈s} f(x).

Русский

Если a ∈ s, то f(a) ≤ ∏_{x∈s} f(x).

LaTeX

$$$ \\forall \\iota\\, N\\, [\\text{CommMonoid } N], [\\text{PartialOrder } N], {f : \\iota \\to N} {s : \\mathrm{Finset} \\iota}, [\\text{MulLeftMono } N], ( h : a \\in s ) \\Rightarrow f(a) \\le \\prod_{x \\in s} f(x). $$$

Lean4

@[to_additive single_le_sum]
theorem single_le_prod' [MulLeftMono N] (hf : ∀ i ∈ s, 1 ≤ f i) {a} (h : a ∈ s) : f a ≤ ∏ x ∈ s, f x :=
  calc
    f a = ∏ i ∈ { a }, f i := (prod_singleton _ _).symm
    _ ≤ ∏ i ∈ s, f i := prod_le_prod_of_subset_of_one_le' (singleton_subset_iff.2 h) fun i hi _ ↦ hf i hi

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