α : Type u_1
β : Type ?u.370021
ι : Type ?u.370024
G : Type ?u.370027
M : Type u_2
N : Type ?u.370033
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
t : Set (Set α)
h : PairwiseDisjoint t id
ht₀ : Set.Finite t
ht₁ : ∀ (x : Set α), x ∈ t → Set.Finite x
⊢ (∏ᶠ (a : α) (_ : a ∈ ⋃ (i : Set α) (_ : i ∈ t), i), f a) = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a
α : Type u_1
β : Type ?u.370021
ι : Type ?u.370024
G : Type ?u.370027
M : Type u_2
N : Type ?u.370033
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
t : Set (Set α)
h : PairwiseDisjoint t id
ht₀ : Set.Finite t
ht₁ : ∀ (x : Set α), x ∈ t → Set.Finite x
⊢ (∏ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a) = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a
rw [Set.sUnion_eq_biUnion]
no goals
α : Type u_1
β : Type ?u.370021
ι : Type ?u.370024
G : Type ?u.370027
M : Type u_2
N : Type ?u.370033
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ : Set α
t : Set (Set α)
h : PairwiseDisjoint t id
ht₀ : Set.Finite t
ht₁ : ∀ (x : Set α), x ∈ t → Set.Finite x
⊢ (∏ᶠ (a : α) (_ : a ∈ ⋃ (i : Set α) (_ : i ∈ t), i), f a) = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a
exact finprod_mem_biUnion h ht₀ ht₁