α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
h : HasBasis (𝓤 α) p s
x : α
⊢ HasBasis (comap (Prod.mk x) (𝓤 α)) p fun i => ball x (s i)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
h : HasBasis (𝓤 α) p s
x : α
⊢ HasBasis (𝓝 x) p fun i => ball x (s i)
rw [nhds_eq_comap_uniformity]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
h : HasBasis (𝓤 α) p s
x : α
⊢ HasBasis (comap (Prod.mk x) (𝓤 α)) p fun i => ball x (s i)
exact h.comap (Prod.mk x)