ι : Type u_1
ι' : Type ?u.1733303
α : ι → Type u_2
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : Set ((i : ι) → α i)
⊢ ∏ i : ι, ↑(m i) ((fun a => a i) '' s) = piPremeasure m s
ι : Type u_1
ι' : Type ?u.1733303
α : ι → Type u_2
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : Set ((i : ι) → α i)
⊢ piPremeasure m (Set.pi univ fun i => eval i '' s) = piPremeasure m s
simp [piPremeasure_pi']
no goals
ι : Type u_1
ι' : Type ?u.1733303
α : ι → Type u_2
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : Set ((i : ι) → α i)
⊢ ∏ i : ι, ↑(m i) ((fun a => a i) '' s) = piPremeasure m s
rfl