α : Type ?u.51011
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x : Γ₀
h : x ≠ 0
⊢ HasBasis (pure x) (fun x => True) fun x_1 => {x}
α : Type ?u.51011
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x : Γ₀
h : x ≠ 0
⊢ HasBasis (𝓝 x) (fun x => True) fun x_1 => {x}
rw [nhds_of_ne_zero h]
no goals
α : Type ?u.51011
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x : Γ₀
h : x ≠ 0
⊢ HasBasis (pure x) (fun x => True) fun x_1 => {x}
exact hasBasis_pure _