α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
l : Filter β
f g : β → α
inst✝ : NoMaxOrder α
a : α
⊢ HasBasis (⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (b - a) < r}) (fun ε => 0 < ε) fun ε => {b | abs (b - a) < ε}
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
l : Filter β
f g : β → α
inst✝ : NoMaxOrder α
a : α
⊢ HasBasis (𝓝 a) (fun ε => 0 < ε) fun ε => {b | abs (b - a) < ε}
simp only [nhds_eq_iInf_abs_sub, abs_sub_comm (a := a)]
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
l : Filter β
f g : β → α
inst✝ : NoMaxOrder α
a x : α
hx : x > 0
y : α
hy : y > 0
⊢ ∃ k, k > 0 ∧ {b | abs (b - a) < k} ⊆ {b | abs (b - a) < x} ∧ {b | abs (b - a) < k} ⊆ {b | abs (b - a) < y}
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
l : Filter β
f g : β → α
inst✝ : NoMaxOrder α
a : α
⊢ HasBasis (⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (b - a) < r}) (fun ε => 0 < ε) fun ε => {b | abs (b - a) < ε}
refine hasBasis_biInf_principal' (fun x hx y hy => ?_) (exists_gt _)
no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
l : Filter β
f g : β → α
inst✝ : NoMaxOrder α
a x : α
hx : x > 0
y : α
hy : y > 0
⊢ ∃ k, k > 0 ∧ {b | abs (b - a) < k} ⊆ {b | abs (b - a) < x} ∧ {b | abs (b - a) < k} ⊆ {b | abs (b - a) < y}
exact ⟨min x y, lt_min hx hy, fun _ hz => hz.trans_le (min_le_left _ _),
  fun _ hz => hz.trans_le (min_le_right _ _)⟩