α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.77543
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ Filter.lift (𝓤 α) (g ∘ preimage (Prod.mk x)) = Filter.lift (𝓤 α) fun s => g (ball x s)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.77543
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ Filter.lift (𝓝 x) g = Filter.lift (𝓤 α) fun s => g (ball x s)
rw [nhds_eq_comap_uniformity, comap_lift_eq2 hg]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.77543
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ Filter.lift (𝓤 α) (g ∘ preimage (Prod.mk x)) = Filter.lift (𝓤 α) fun s => g (ball x s)
rfl