hasProd_le — Mathlib

English

If every term-wise bound f(i) ≤ g(i) holds and HasProd f a and HasProd g b converge, then a ≤ b.

Русский

Если для всех i имеем f(i) ≤ g(i) и сходятся произведения HasProd f a и HasProd g b, то a ≤ b.

LaTeX

$$$\\displaystyle (\\forall i, f(i) \\le g(i)) \\rightarrow \\text{HasProd } f\\ a\\ L \\rightarrow \\text{HasProd } g\\ b\\ L \\rightarrow a \\le b$$$

Lean4

@[to_additive]
theorem hasProd_le (h : ∀ i, f i ≤ g i) (hf : HasProd f a₁ L) (hg : HasProd g a₂ L) [L.NeBot] : a₁ ≤ a₂ :=
  le_of_tendsto_of_tendsto' hf hg fun _ ↦ prod_le_prod' fun i _ ↦ h i

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