English
If f is locally finite, then the neighborhood filter within the union equals the supremum of neighborhood filters within each f_i.
Русский
Если f локально конечна, то фильтр окрестностей внутри объединения равен верхней границе фильтров окрестностей внутри каждого f_i.
LaTeX
$$LocallyFinite f → ∀ a, 𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a$$
Lean4
protected theorem nhdsWithin_iUnion (hf : LocallyFinite f) (a : X) : 𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a :=
by
rcases hf a with ⟨U, haU, hfin⟩
refine le_antisymm ?_ (Monotone.le_map_iSup fun _ _ ↦ nhdsWithin_mono _)
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
