prod_le_one

Mathlib.Algebra.Order.BigOperators.Group.Finset

URI: https://scilib.ai/kg/mathlib#Fintype.prod_le_one

English

If f(i) ≤ 1 for all i, then ∏ i f(i) ≤ 1.

Русский

Если для всех i выполняется f(i) ≤ 1, то произведение ≤ 1.

LaTeX

$$$\left( \forall i, f(i) \le 1 \right) \Rightarrow \prod_{i} f(i) \le 1$$$

Lean4

@[to_additive]
theorem prod_le_one (hf : f ≤ 1) : ∏ i, f i ≤ 1 :=
  Finset.prod_le_one' fun _ _ ↦ hf _

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

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

Разделы

Аффилиация

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