case h
ι : Type u_1
ι' : Type ?u.7433
α : Type ?u.7436
X : Type u_2
Y : Type ?u.7442
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
h : LocallyFinite f
x : X
⊢ x ∈ closure (⋃ (i : ι), f i) ↔ x ∈ ⋃ (i : ι), closure (f i)
ι : Type u_1
ι' : Type ?u.7433
α : Type ?u.7436
X : Type u_2
Y : Type ?u.7442
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
h : LocallyFinite f
⊢ closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
ext x
no goals
case h
ι : Type u_1
ι' : Type ?u.7433
α : Type ?u.7436
X : Type u_2
Y : Type ?u.7442
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
h : LocallyFinite f
x : X
⊢ x ∈ closure (⋃ (i : ι), f i) ↔ x ∈ ⋃ (i : ι), closure (f i)
simp only [mem_closure_iff_nhdsWithin_neBot, h.nhdsWithin_iUnion, iSup_neBot, mem_iUnion]