case intro.intro
ι : Type u_1
ι' : Type ?u.3024
α : Type ?u.3027
X : Type u_2
Y : Type ?u.3033
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite {i | Set.Nonempty (f i ∩ U)}
⊢ 𝓝[⋃ (i : ι), f i] a = ⨆ (i : ι), 𝓝[f i] a
ι : Type u_1
ι' : Type ?u.3024
α : Type ?u.3027
X : Type u_2
Y : Type ?u.3033
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
⊢ 𝓝[⋃ (i : ι), f i] a = ⨆ (i : ι), 𝓝[f i] a
rcases hf a with ⟨U, haU, hfin⟩
case intro.intro
ι : Type u_1
ι' : Type ?u.3024
α : Type ?u.3027
X : Type u_2
Y : Type ?u.3033
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite {i | Set.Nonempty (f i ∩ U)}
⊢ 𝓝[⋃ (i : ι), f i] a ≤ ⨆ (i : ι), 𝓝[f i] a
case intro.intro
ι : Type u_1
ι' : Type ?u.3024
α : Type ?u.3027
X : Type u_2
Y : Type ?u.3033
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite {i | Set.Nonempty (f i ∩ U)}
⊢ 𝓝[⋃ (i : ι), f i] a = ⨆ (i : ι), 𝓝[f i] a
refine le_antisymm ?_ (Monotone.le_map_iSup fun _ _ ↦ nhdsWithin_mono _)
no goals
case intro.intro
ι : Type u_1
ι' : Type ?u.3024
α : Type ?u.3027
X : Type u_2
Y : Type ?u.3033
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite {i | Set.Nonempty (f i ∩ U)}
⊢ 𝓝[⋃ (i : ι), f i] a ≤ ⨆ (i : ι), 𝓝[f i] a
calc
  𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a := by
    rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
  _ = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, (f i ∩ U)] a := by
    simp only [mem_setOf_eq, iUnion_nonempty_self]
  _ = ⨆ i ∈ {j | (f j ∩ U).Nonempty}, 𝓝[f i ∩ U] a := nhdsWithin_biUnion hfin _ _
  _ ≤ ⨆ i, 𝓝[f i ∩ U] a := iSup₂_le_iSup _ _
  _ ≤ ⨆ i, 𝓝[f i] a := iSup_mono fun i ↦ nhdsWithin_mono _ <| inter_subset_left _ _
no goals
ι : Type u_1
ι' : Type ?u.3024
α : Type ?u.3027
X : Type u_2
Y : Type ?u.3033
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite {i | Set.Nonempty (f i ∩ U)}
⊢ 𝓝[⋃ (i : ι), f i] a = 𝓝[⋃ (i : ι), f i ∩ U] a
rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
no goals
ι : Type u_1
ι' : Type ?u.3024
α : Type ?u.3027
X : Type u_2
Y : Type ?u.3033
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite {i | Set.Nonempty (f i ∩ U)}
⊢ 𝓝[⋃ (i : ι), f i ∩ U] a = 𝓝[⋃ (i : ι) (_ : i ∈ {j | Set.Nonempty (f j ∩ U)}), f i ∩ U] a
simp only [mem_setOf_eq, iUnion_nonempty_self]