case h.e'_3
α : Type u
β : Type v
ι : Type u_2
π : ι → Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
h : ∀ (i : ι), IsCompact (s i)
⊢ Set.pi univ s = {x | ∀ (i : ι), x i ∈ s i}
α : Type u
β : Type v
ι : Type u_2
π : ι → Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
h : ∀ (i : ι), IsCompact (s i)
⊢ IsCompact (Set.pi univ s)
convert isCompact_pi_infinite h
no goals
case h.e'_3
α : Type u
β : Type v
ι : Type u_2
π : ι → Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
h : ∀ (i : ι), IsCompact (s i)
⊢ Set.pi univ s = {x | ∀ (i : ι), x i ∈ s i}
simp only [← mem_univ_pi, setOf_mem_eq]