tprod_mono

Mathlib.Topology.Algebra.InfiniteSum.Order

URI: https://scilib.ai/kg/mathlib#Multipliable.tprod_mono

← MathLib Explorer

English

If f < g pointwise, then tprod f < tprod g.

Русский

Если f < g по каждому индексу, то tprod f < tprod g.

LaTeX

$$$\\forall f,g:\\, \\text{HasProd } f a_1 L \\to \\text{HasProd } g a_2 L \\to \\Pi.preorder.lt f g \\to a_1 < a_2$$$

Lean4

@[to_additive (attr := mono)]
protected theorem tprod_mono [L.NeBot] (hf : Multipliable f L) (hg : Multipliable g L) (h : f ≤ g) :
    ∏'[L] n, f n ≤ ∏'[L] n, g n :=
  hf.tprod_le_tprod h hg

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru