α : Type u
β : Type v
X : Type ?u.49037
ι : Type ?u.49040
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
⊢ HasBasis (𝓤 α) (fun ε => 0 < ε) fun ε => {p | dist p.fst p.snd < ε}
α : Type u
β : Type v
X : Type ?u.49037
ι : Type ?u.49040
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
⊢ HasBasis (𝓤 α) (fun ε => 0 < ε) fun ε => {p | dist p.fst p.snd < ε}
rw [toUniformSpace_eq]
no goals
α : Type u
β : Type v
X : Type ?u.49037
ι : Type ?u.49040
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
⊢ HasBasis (𝓤 α) (fun ε => 0 < ε) fun ε => {p | dist p.fst p.snd < ε}
exact UniformSpace.hasBasis_ofFun (exists_gt _) _ _ _ _ _