α✝ : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α✝
inst✝³ : LinearOrderedAddCommGroup α✝
inst✝² : OrderTopology α✝
l : Filter β
f g : β → α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}
a : α
⊢ 𝓝 a = 𝓝 a
α✝ : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α✝
inst✝³ : LinearOrderedAddCommGroup α✝
inst✝² : OrderTopology α✝
l : Filter β
f g : β → α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}
⊢ OrderTopology α
refine' ⟨eq_of_nhds_eq_nhds fun a => _⟩
α✝ : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α✝
inst✝³ : LinearOrderedAddCommGroup α✝
inst✝² : OrderTopology α✝
l : Filter β
f g : β → α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}
a : α
⊢ (⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}) = 𝓝 a
α✝ : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α✝
inst✝³ : LinearOrderedAddCommGroup α✝
inst✝² : OrderTopology α✝
l : Filter β
f g : β → α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}
a : α
⊢ 𝓝 a = 𝓝 a
rw [h_nhds]
α✝ : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α✝
inst✝³ : LinearOrderedAddCommGroup α✝
inst✝² : OrderTopology α✝
l : Filter β
f g : β → α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}
a : α
this : TopologicalSpace α := Preorder.topology α
⊢ (⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}) = 𝓝 a
α✝ : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α✝
inst✝³ : LinearOrderedAddCommGroup α✝
inst✝² : OrderTopology α✝
l : Filter β
f g : β → α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}
a : α
⊢ (⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}) = 𝓝 a
letI := Preorder.topology α
α✝ : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α✝
inst✝³ : LinearOrderedAddCommGroup α✝
inst✝² : OrderTopology α✝
l : Filter β
f g : β → α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}
a : α
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α := { topology_eq_generate_intervals := rfl }
⊢ (⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}) = 𝓝 a
α✝ : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α✝
inst✝³ : LinearOrderedAddCommGroup α✝
inst✝² : OrderTopology α✝
l : Filter β
f g : β → α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}
a : α
this : TopologicalSpace α := Preorder.topology α
⊢ (⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}) = 𝓝 a
letI : OrderTopology α := ⟨rfl⟩
no goals
α✝ : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α✝
inst✝³ : LinearOrderedAddCommGroup α✝
inst✝² : OrderTopology α✝
l : Filter β
f g : β → α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}
a : α
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α := { topology_eq_generate_intervals := rfl }
⊢ (⨅ (r : α) (_ : r > 0), 𝓟 {b | abs (a - b) < r}) = 𝓝 a
exact (nhds_eq_iInf_abs_sub a).symm