α : Type ?u.3501
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ HasBasis (⨅ (γ : Γ₀) (_ : γ ≠ 0), 𝓟 (Iio γ)) (fun γ => γ ≠ 0) Iio
α : Type ?u.3501
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ HasBasis (𝓝 0) (fun γ => γ ≠ 0) Iio
rw [nhds_zero]
α : Type ?u.3501
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ DirectedOn ((fun γ => Iio γ) ⁻¹'o fun x x_1 => x ≥ x_1) fun γ => γ = 0 → False
α : Type ?u.3501
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ HasBasis (⨅ (γ : Γ₀) (_ : γ ≠ 0), 𝓟 (Iio γ)) (fun γ => γ ≠ 0) Iio
refine' hasBasis_biInf_principal _ ⟨1, one_ne_zero⟩
no goals
α : Type ?u.3501
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ DirectedOn ((fun γ => Iio γ) ⁻¹'o fun x x_1 => x ≥ x_1) fun γ => γ = 0 → False
exact directedOn_iff_directed.2 (directed_of_inf fun a b hab => Iio_subset_Iio hab)