English
Let α be a uniform space. For monotone g, the lift of nhds x equals the lift of the uniformity with a preimage of the diagonal: (nhds x).lift g = (𝓤 α).lift (λ s, g {y | (y, x) ∈ s}).
Русский
Пусть α — равномерное пространство. Для монотонного g выполняется (nhds x).lift g = (𝓤 α).lift (λ s, g {y | (y, x) ∈ s}).
LaTeX
$$$ (\mathcal{N}(x)).\mathrm{lift}\, g = (\mathcal{U}(\alpha)).\mathrm{lift} \; (\lambda s : \mathcal{P}(\alpha \times \alpha), g\{y \mid (y, x) \in s\}) $$$
Lean4
theorem lift_nhds_right {x : α} {g : Set α → Filter β} (hg : Monotone g) :
(𝓝 x).lift g = (𝓤 α).lift fun s : Set (α × α) => g {y | (y, x) ∈ s} :=
by
rw [nhds_eq_comap_uniformity', comap_lift_eq2 hg]
simp_rw [Function.comp_def, preimage]
