prod_mono' — Mathlib

English

For a finite index type, the map f ↦ ∏ i f(i) is monotone with respect to the pointwise order: if f ≤ g, then ∏ i f(i) ≤ ∏ i g(i).

Русский

Отображение f ↦ ∏_i f(i) монотонно по точечной порядку: если f ≤ g, то произведение ≤ произведение g.

LaTeX

$$$f \le g \implies \prod_{i} f(i) \le \prod_{i} g(i)$$$

Lean4

@[to_additive (attr := mono) sum_mono]
theorem prod_mono' : Monotone fun f : ι → M ↦ ∏ i, f i := fun _ _ hfg ↦ Finset.prod_le_prod' fun x _ ↦ hfg x

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