le_one

Mathlib.Topology.Algebra.InfiniteSum.Order

URI: https://scilib.ai/kg/mathlib#HasProd.le_one

English

If every g i ≥ 1 and HasProd g a L holds, then a ≥ 1.

Русский

Если каждый g i ≥ 1 и HasProd g a L, то a ≥ 1.

LaTeX

$$$\\forall g:\\, ι \\to α, (\\forall i, g i \\ge 1) \\to \\text{HasProd } g a L \\to a \\ge 1$$$

Lean4

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

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

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

Разделы

Аффилиация

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