finprod_of_infinite_mulSupport

Mathlib.Algebra.BigOperators.Finprod

URI: https://scilib.ai/kg/mathlib#finprod_of_infinite_mulSupport

← MathLib Explorer

English

If mulSupport f is infinite, then the finprod of f is 1.

Русский

Если опора mulSupport f бесконечна, то финпроизводство f равно 1.

LaTeX

$$$$ \text{If } (\mathrm{mulSupport} f).\mathrm{Infinite}, \quad \prod^{\mathrm{fin}}_{i} f(i) = 1. $$$$

Lean4

@[to_additive]
theorem finprod_of_infinite_mulSupport {f : α → M} (hf : (mulSupport f).Infinite) : ∏ᶠ i, f i = 1 := by
  classical rw [finprod_def, dif_neg hf]

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

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

Разделы

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

Аффилиация

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