no goals
α : Type u_2
β : Type ?u.1617
γ : Type ?u.1620
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
f : ι → Set α
hf : ∀ (i : ι), IsOpen (f i)
⊢ ∀ (t : Set α), t ∈ range f → IsOpen t
rwa [forall_range_iff]
no goals
α : Type u_2
β : Type ?u.1617
γ : Type ?u.1620
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
f : ι → Set α
hf : ∀ (i : ι), IsOpen (f i)
⊢ (⋂ (i : ι), f i) = ⋂₀ range f
rw [sInter_range]