prod_le_prod_of_subset' — Mathlib

English

If s ⊆ t, then ∏_{x ∈ s} f(x) ≤ ∏_{x ∈ t} f(x), provided f(x) ≥ 1 for all x.

Русский

Если s ⊆ t и f(x) ≥ 1 для всех x, то произведение по s не превосходит по t.

LaTeX

$$$s \\subseteq t \\land (\\forall x ∈ s, f(x) \\ge 1) \\Rightarrow \\prod_{x ∈ s} f(x) ≤ \\prod_{x ∈ t} f(x)$$$

Lean4

@[to_additive sum_le_sum_of_subset]
theorem prod_le_prod_of_subset' (h : s ⊆ t) : ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x :=
  have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
  prod_le_prod_of_subset_of_one_le' h fun _ _ _ ↦ one_le _

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