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 PredOrder.isOpen_singleton_of_not_isPredPrelimit {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {a : α} [PredOrder α] (ha : ¬Order.IsPredPrelimit a) : IsOpen {a}

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

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

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

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

theorem SuccOrder.nhds_of_isMin {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α] {a : α} (h : IsMin a) : nhds a = pure a

theorem PredOrder.nhds_of_isMax {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α] {a : α} (h : IsMax a) : nhds a = pure a

@[simp]

theorem SuccOrder.nhds_bot {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α] [OrderBot α] : nhds ⊥ = pure ⊥

@[simp]

theorem PredOrder.nhds_top {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α] [OrderTop α] : nhds ⊤ = pure ⊤

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 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 SuccOrder.accPt_principal {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α] {a : α} {s : Set α} : AccPt a (Filter.principal s) ↔ ¬IsMin a ∧ ∀ b < a, (s ∩ Set.Ioo b a).Nonempty

theorem PredOrder.accPt_principal {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α] {a : α} {s : Set α} : AccPt a (Filter.principal s) ↔ ¬IsMax a ∧ ∀ (b : α), a < b → (s ∩ Set.Ioo a b).Nonempty

theorem AccPt.not_isMin {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α] {a : α} {s : Set α} (h : AccPt a (Filter.principal s)) : ¬IsMin a

theorem AccPt.not_isMax {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α] {a : α} {s : Set α} (h : AccPt a (Filter.principal s)) : ¬IsMax a

theorem AccPt.isSuccLimit {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α] {a : α} {s : Set α} (h : AccPt a (Filter.principal s)) : Order.IsSuccLimit a

theorem AccPt.isPredLimit {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α] {a : α} {s : Set α} (h : AccPt a (Filter.principal s)) : Order.IsPredLimit a

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.isPredLimit_of_mem_frontier {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α] {a : α} {s : Set α} (ha : a ∈ frontier s) : Order.IsPredLimit a