α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
a : α
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}}), 𝓟 s) =
    (⨅ (b : α) (_ : b ∈ Iio a), 𝓟 (Ioi b)) ⊓ ⨅ (b : α) (_ : b ∈ Ioi a), 𝓟 (Iio b)
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
a : α
⊢ 𝓝 a = (⨅ (b : α) (_ : b ∈ Iio a), 𝓟 (Ioi b)) ⊓ ⨅ (b : α) (_ : b ∈ Ioi a), 𝓟 (Iio b)
rw [t.topology_eq_generate_intervals, nhds_generateFrom]
no goals
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
a : α
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}}), 𝓟 s) =
    (⨅ (b : α) (_ : b ∈ Iio a), 𝓟 (Ioi b)) ⊓ ⨅ (b : α) (_ : b ∈ Ioi a), 𝓟 (Iio b)
simp_rw [mem_setOf_eq, @and_comm (a ∈ _), exists_or, or_and_right, iInf_or, iInf_and, iInf_exists,
  iInf_inf_eq, iInf_comm (ι := Set α), iInf_iInf_eq_left, mem_Ioi, mem_Iio]