English
Let α be a uniform space. For any monotone map g from subsets of α to filters on β, the lift of the neighborhood filter at x equals the lift of the uniformity: (nhds x).lift g = (𝓤 α).lift (λ s, g (ball x s)).
Русский
Пусть α — равномерное пространство. Для монотонного отображения g из подмножеств α в фильтры на β выполняется равенство: (nhds x).lift g = (𝓤 α).lift (λ s, g (ball x s)).
LaTeX
$$$ (\mathcal{N}(x)).\mathrm{lift}\, g = (\mathcal{U}(\alpha)).\mathrm{lift} \; (\lambda s : \mathcal{P}(\alpha \times \alpha),\; g(\mathrm{ball}(x,s))) $$$
Lean4
theorem lift_nhds_left {x : α} {g : Set α → Filter β} (hg : Monotone g) :
(𝓝 x).lift g = (𝓤 α).lift fun s : Set (α × α) => g (ball x s) :=
by
rw [nhds_eq_comap_uniformity, comap_lift_eq2 hg]
simp_rw [ball, Function.comp_def]
