le_tprod' — Mathlib

English

Let f: ι → α be a multipliable family in a canonically ordered monoid α with a suitable topology. Then for every index i, the value f(i) is bounded above by the infinite product ∏' j, f(j).

Русский

Пусть f: ι → α — функция в упорядоченном мульдоображении α с подходящей топологией; тогда для любого индекса i выполняется неравенство f(i) ≤ ∏' j, f(j).

LaTeX

$$$\\\\forall i \\, f(i) \\\\le \\, \prod' j, f(j)$$$

Lean4

@[to_additive]
protected theorem le_tprod' (hf : Multipliable f) (i : ι) : f i ≤ ∏' i, f i :=
  hf.le_tprod i fun _ _ ↦ one_le _

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