prod_lt_one_iff_of_le_one

Mathlib.Algebra.Order.BigOperators.Group.Finset

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

English

If f ≤ 1, then ∏ f i < 1 iff f < 1 (i.e., there exists i with f(i) < 1).

Русский

Если f ≤ 1, тогда ∏ f i < 1 тогда и только тогда, когда f < 1.

LaTeX

$$$f \le 1 \implies \left( \prod_i f(i) < 1 \iff f < 1 \right)$$$

Lean4

@[to_additive]
theorem prod_lt_one_iff_of_le_one (hf : f ≤ 1) : ∏ i, f i < 1 ↔ f < 1 := by
  obtain rfl | hf := hf.eq_or_lt <;> simp [*, prod_lt_one]

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

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

Разделы

Аффилиация

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