α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ ∀ (i : α), x i ∈ ↑(t i)
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ x ∈ Set.pi Set.univ fun a => ↑(t a)
rw [Set.mem_univ_pi]
no goals
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_1
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ ∀ (i : α), x i ∈ ↑(t i)
exact Fintype.mem_piFinset