English
For a family of measures μ_i and Encodable index set, pi' μ evaluated on the product of sets equals the product of μ_i on each coordinate, under nonempty condition.
Русский
Для семейства мер μ_i и кодируемого множества индексов, значение pi' μ на произведении множеств равно произведению μ_i на каждой координате (при непустости).
LaTeX
$$\pi'(μ)(\pi univ s) = ∏_i μ_i(s_i)$$
Lean4
theorem piPremeasure_pi' {s : ∀ i, Set (α i)} : piPremeasure m (pi univ s) = ∏ i, m i (s i) :=
by
cases isEmpty_or_nonempty ι
· simp [piPremeasure]
rcases (pi univ s).eq_empty_or_nonempty with h | h
· rcases univ_pi_eq_empty_iff.mp h with ⟨i, hi⟩
have : ∃ i, m i (s i) = 0 := ⟨i, by simp [hi]⟩
simpa [h, Finset.card_univ, zero_pow Fintype.card_ne_zero, @eq_comm _ (0 : ℝ≥0∞), Finset.prod_eq_zero_iff,
piPremeasure]
· simp [h, piPremeasure]
