no goals
α : Type u_2
β : Type ?u.1242
γ : Type ?u.1245
ι : Type u_1
inst✝ : TopologicalSpace α
I : Set ι
hI : Set.Countable I
f : ι → Set α
hf : ∀ (i : ι), i ∈ I → IsOpen (f i)
⊢ ∀ (t : Set α), t ∈ f '' I → IsOpen t
rwa [ball_image_iff]
no goals
α : Type u_2
β : Type ?u.1242
γ : Type ?u.1245
ι : Type u_1
inst✝ : TopologicalSpace α
I : Set ι
hI : Set.Countable I
f : ι → Set α
hf : ∀ (i : ι), i ∈ I → IsOpen (f i)
⊢ (⋂ (i : ι) (_ : i ∈ I), f i) = ⋂₀ (f '' I)
rw [sInter_image]