infinitePi_eq_pi

Mathlib.Probability.ProductMeasure

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.infinitePi_eq_pi

← MathLib Explorer

English

If ι is finite, infinitePi μ equals the finite product pi μ.

Русский

Если индексный набор конечен, infinitePi μ равен конечному произведению μ.

LaTeX

$$$$[\text{Fintype }\iota] \Rightarrow \mathrm{infinitePi}\;μ = \mathrm{pi}\;μ.$$$$

Lean4

theorem infinitePi_eq_pi [Fintype ι] : infinitePi μ = Measure.pi μ :=
  by
  refine (pi_eq fun s hs ↦ ?_).symm
  rw [← coe_univ, infinitePi_pi]
  simpa

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

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

Разделы

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

Аффилиация

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