case h
α : Type u
β : Type v
γ : Type ?u.313054
δ : Type ?u.313057
ε : Type ?u.313060
ζ : Type ?u.313063
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.313074
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
I : Set ι
hI : Set.Finite I
s : (i : ι) → Set (π i)
a : (i : ι) → π i
⊢ a ∈ interior (Set.pi I s) ↔ a ∈ Set.pi I fun i => interior (s i)
α : Type u
β : Type v
γ : Type ?u.313054
δ : Type ?u.313057
ε : Type ?u.313060
ζ : Type ?u.313063
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.313074
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
I : Set ι
hI : Set.Finite I
s : (i : ι) → Set (π i)
⊢ interior (Set.pi I s) = Set.pi I fun i => interior (s i)
ext a
no goals
case h
α : Type u
β : Type v
γ : Type ?u.313054
δ : Type ?u.313057
ε : Type ?u.313060
ζ : Type ?u.313063
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.313074
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
I : Set ι
hI : Set.Finite I
s : (i : ι) → Set (π i)
a : (i : ι) → π i
⊢ a ∈ interior (Set.pi I s) ↔ a ∈ Set.pi I fun i => interior (s i)
simp only [Set.mem_pi, mem_interior_iff_mem_nhds, set_pi_mem_nhds_iff hI]