Order topologies of successor or predecessor orders

This file proves miscellaneous results under the assumption of OrderTopology plus either of SuccOrder or PredOrder.

theorem SuccOrder.isOpen_singleton_of_not_isSuccPrelimit {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {a : α} [SuccOrder α] (ha : ¬Order.IsSuccPrelimit a) : IsOpen {a}

theorem SuccOrder.isOpen_singleton_iff {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {a : α} [SuccOrder α] [NoMaxOrder α] : IsOpen {a} ↔ ¬Order.IsSuccLimit a

theorem SuccOrder.nhds_eq_pure {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α] {a : α} : nhds a = pure a ↔ ¬Order.IsSuccLimit a

theorem SuccOrder.isOpen_iff {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α] {s : Set α} : IsOpen s ↔ ∀ o ∈ s, Order.IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s

theorem SuccOrder.isSuccLimit_of_mem_frontier {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α] {a : α} {s : Set α} (ha : a ∈ frontier s) : Order.IsSuccLimit a

theorem PredOrder.isOpen_singleton_of_not_isPredPrelimit {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {a : α} [PredOrder α] (ha : ¬Order.IsPredPrelimit a) : IsOpen {a}

theorem PredOrder.isOpen_singleton_iff {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {a : α} [PredOrder α] [NoMinOrder α] : IsOpen {a} ↔ ¬Order.IsPredLimit a

theorem PredOrder.nhds_eq_pure {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α] {a : α} : nhds a = pure a ↔ ¬Order.IsPredLimit a

theorem PredOrder.isOpen_iff {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α] {s : Set α} : IsOpen s ↔ ∀ o ∈ s, Order.IsPredLimit o → ∃ (a : α), o < a ∧ Set.Ioo o a ⊆ s

theorem PredOrder.isPredLimit_of_mem_frontier {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α] {a : α} {s : Set α} (ha : a ∈ frontier s) : Order.IsPredLimit a