one_le — Mathlib

English

If Multipliable f L and h_i ≤ h_j for i ≤ j in a sense, then the tprod is monotone with respect to a pointwise bound.

Русский

Если f снова монотонно ограничено, то tprod монотонно возрастает.

LaTeX

$$$\\forall f,g:\\, (\\forall i, f(i) ≤ g(i)) \\to \\text{Multipliable } f L \\to \\text{Multipliable } g L \\to (\\text{tprod } f L) ≤ (\\text{tprod } g L)$$$

Lean4

@[to_additive]
theorem one_le [L.NeBot] (h : ∀ i, 1 ≤ g i) (ha : HasProd g a L) : 1 ≤ a :=
  hasProd_le h hasProd_one ha

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