prod_strictMono' — Mathlib

English

The map f ↦ ∏ i f(i) is strictly monotone with respect to the pointwise order on functions: if f < g, then ∏ i f(i) < ∏ i g(i).

Русский

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

LaTeX

$$$f < g \Rightarrow \prod_i f(i) < \prod_i g(i)$$$

Lean4

@[to_additive sum_strictMono]
theorem prod_strictMono' : StrictMono fun f : ι → M ↦ ∏ x, f x := fun _ _ hfg ↦
  let ⟨hle, i, hlt⟩ := Pi.lt_def.mp hfg
  Finset.prod_lt_prod' (fun i _ ↦ hle i) ⟨i, Finset.mem_univ i, hlt⟩

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