le_hasProd'

Mathlib.Topology.Algebra.InfiniteSum.Order

URI: https://scilib.ai/kg/mathlib#le_hasProd'

English

If HasProd f a and for each i, 1 ≤ f i, then f i ≤ a for all i.

Русский

Если HasProd f a и для каждого i выполняется 1 ≤ f i, тогда f i ≤ a для всех i.

LaTeX

$$$\\forall f a L,\\, \\text{HasProd } f a L \\to \\forall i, f(i) \\le a$$$

Lean4

@[to_additive]
theorem le_hasProd' (hf : HasProd f a) (i : ι) : f i ≤ a :=
  le_hasProd hf i fun _ _ ↦ one_le _

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

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

Разделы

Аффилиация

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