R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ Filter.HasBasis (Filter.comap (fun x => x.snd - x.fst) (𝓝 0)) (fun x => True) fun γ => {p | ↑v (p.snd - p.fst) < ↑γ}
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ Filter.HasBasis (uniformity R) (fun x => True) fun γ => {p | ↑v (p.snd - p.fst) < ↑γ}
rw [uniformity_eq_comap_nhds_zero]
no goals
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ Filter.HasBasis (Filter.comap (fun x => x.snd - x.fst) (𝓝 0)) (fun x => True) fun γ => {p | ↑v (p.snd - p.fst) < ↑γ}
exact (hasBasis_nhds_zero R Γ₀).comap _