English
If f ≤ g pointwise and e:ι→κ is injective with g controlled away from the range of e, then the infinite products satisfy tprod f ≤ tprod g.
Русский
Если f ≤ g поэлементно и e: ι → κ безусловно инъекция, а значения вне диапазона e удовлетворяют условию, то произведения tprod удовлетворяют tprod f ≤ tprod g.
LaTeX
$$$\\forall f,g,e:\\, \\text{Injective } e\\to (\\forall c, c \\notin \\mathrm{range}(e) \\to 1 \\le g(c)) \\to (\\forall i, f(i) \\le g(e(i))) \\to \\text{Multipliable } f \\to \\text{Multipliable } g \\to \\text{tprod } f \\le \\text{tprod } g$$$
Lean4
@[to_additive]
protected theorem tprod_le_tprod_of_inj {g : κ → α} (e : ι → κ) (he : Injective e) (hs : ∀ c, c ∉ Set.range e → 1 ≤ g c)
(h : ∀ i, f i ≤ g (e i)) (hf : Multipliable f) (hg : Multipliable g) : tprod f ≤ tprod g :=
hasProd_le_inj _ he hs h hf.hasProd hg.hasProd
