α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
x : α
h : HasBasis (comap Prod.swap (𝓤 α)) p fun i => Prod.swap ⁻¹' s i
⊢ HasBasis (𝓝 x) p fun i => {y | (y, 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 => {y | (y, x) ∈ s i}
replace h := h.comap Prod.swap
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
x : α
h : HasBasis (𝓤 α) p fun i => Prod.swap ⁻¹' s i
⊢ HasBasis (𝓝 x) p fun i => {y | (y, x) ∈ s i}
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
x : α
h : HasBasis (comap Prod.swap (𝓤 α)) p fun i => Prod.swap ⁻¹' s i
⊢ HasBasis (𝓝 x) p fun i => {y | (y, x) ∈ s i}
rw [← map_swap_eq_comap_swap, ← uniformity_eq_symm] at h
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
x : α
h : HasBasis (𝓤 α) p fun i => Prod.swap ⁻¹' s i
⊢ HasBasis (𝓝 x) p fun i => {y | (y, x) ∈ s i}
exact nhds_basis_uniformity' h