no goals
α : Type u_2
β : Type ?u.14101
γ : Type ?u.14104
δ : Type ?u.14107
inst✝ : TopologicalSpace α
ι : Type u_1
I : Set ι
hI : Set.Finite I
s : ι → Set α
a : α
⊢ 𝓝[⋃ (i : ι) (_ : i ∈ ∅), s i] a = ⨆ (i : ι) (_ : i ∈ ∅), 𝓝[s i] a
simp
no goals
α : Type u_2
β : Type ?u.14101
γ : Type ?u.14104
δ : Type ?u.14107
inst✝ : TopologicalSpace α
ι : Type u_1
I : Set ι
hI : Set.Finite I
s : ι → Set α
a : α
a✝ : ι
s✝ : Set ι
x✝¹ : ¬a✝ ∈ s✝
x✝ : Set.Finite s✝
hT : 𝓝[⋃ (i : ι) (_ : i ∈ s✝), s i] a = ⨆ (i : ι) (_ : i ∈ s✝), 𝓝[s i] a
⊢ 𝓝[⋃ (i : ι) (_ : i ∈ insert a✝ s✝), s i] a = ⨆ (i : ι) (_ : i ∈ insert a✝ s✝), 𝓝[s i] a
simp only [hT, nhdsWithin_union, iSup_insert, biUnion_insert]