Documentation

Mathlib.Topology.Order.SuccPred

Order topologies of successor or predecessor orders #

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

source
theorem SuccOrder.isOpen_Iic {α : Type u_1} [LinearOrder α] [TopologicalSpace α] {a : α} [SuccOrder α] [ClosedIciTopology α] :
IsOpen (Set.Iic a)
source
theorem PredOrder.isOpen_Ici {α : Type u_1} [LinearOrder α] [TopologicalSpace α] {a : α} [PredOrder α] [ClosedIicTopology α] :
IsOpen (Set.Ici a)
source
theorem SuccOrder.isOpen_Ioc {α : Type u_1} [LinearOrder α] [TopologicalSpace α] {a b : α} [SuccOrder α] [OrderTopology α] :
IsOpen (Set.Ioc a b)
source
theorem PredOrder.isOpen_Ico {α : Type u_1} [LinearOrder α] [TopologicalSpace α] {a b : α} [PredOrder α] [OrderTopology α] :
IsOpen (Set.Ico b a)
source
theorem SuccOrder.isOpen_singleton_iff {α : Type u_1} [LinearOrder α] [TopologicalSpace α] {a : α} [SuccOrder α] [OrderTopology α] :
IsOpen {a} ↔ ¬Order.IsSuccLimit a

In a successor order, limit points correspond to limit successors.

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

In a predecessor order, limit points correspond to limit predecessors.

source
theorem SuccOrder.isOpen_singleton_of_not_isSuccLimit {α : Type u_1} [LinearOrder α] [TopologicalSpace α] {a : α} [SuccOrder α] [OrderTopology α] :
¬Order.IsSuccLimit a → IsOpen {a}

Alias of the reverse direction of SuccOrder.isOpen_singleton_iff.

In a successor order, limit points correspond to limit successors.

source
theorem PredOrder.isOpen_singleton_of_not_isPredLimit {α : Type u_1} [LinearOrder α] [TopologicalSpace α] {a : α} [PredOrder α] [OrderTopology α] :
¬Order.IsPredLimit a → IsOpen {a}

Alias of the reverse direction of PredOrder.isOpen_singleton_iff.

In a predecessor order, limit points correspond to limit predecessors.

source
@[deprecated SuccOrder.isOpen_singleton_of_not_isSuccLimit (since := "2026-11-03")]
theorem SuccOrder.isOpen_singleton_of_not_isSuccPrelimit {α : Type u_1} [LinearOrder α] [TopologicalSpace α] {a : α} [SuccOrder α] [OrderTopology α] (ha : ¬Order.IsSuccPrelimit a) :
IsOpen {a}
source
@[deprecated PredOrder.isOpen_singleton_of_not_isPredLimit (since := "2026-11-03")]
theorem PredOrder.isOpen_singleton_of_not_isPredPrelimit {α : Type u_1} [LinearOrder α] [TopologicalSpace α] {a : α} [PredOrder α] [OrderTopology α] (ha : ¬Order.IsPredPrelimit a) :
IsOpen {a}
source
theorem SuccOrder.isOpen_singleton_of_isMin {α : Type u_1} [LinearOrder α] [TopologicalSpace α] {a : α} [SuccOrder α] [OrderTopology α] (ha : IsMin a) :
IsOpen {a}
source
theorem PredOrder.isOpen_singleton_of_isMax {α : Type u_1} [LinearOrder α] [TopologicalSpace α] {a : α} [PredOrder α] [OrderTopology α] (ha : IsMax a) :
IsOpen {a}
source
@[simp]
theorem SuccOrder.isOpen_singleton_bot {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [SuccOrder α] [OrderTopology α] [OrderBot α] :
IsOpen {⊥}
source
@[simp]
theorem PredOrder.isOpen_singleton_top {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [PredOrder α] [OrderTopology α] [OrderTop α] :
IsOpen {⊤}
source
theorem SuccOrder.nhds_eq_pure {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [SuccOrder α] [OrderTopology α] {a : α} :
nhds a = pure a ↔ ¬Order.IsSuccLimit a
source
theorem PredOrder.nhds_eq_pure {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [PredOrder α] [OrderTopology α] {a : α} :
nhds a = pure a ↔ ¬Order.IsPredLimit a
source
theorem SuccOrder.nhds_of_isMin {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [SuccOrder α] [OrderTopology α] {a : α} (h : IsMin a) :
nhds a = pure a
source
theorem PredOrder.nhds_of_isMax {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [PredOrder α] [OrderTopology α] {a : α} (h : IsMax a) :
nhds a = pure a
source
@[simp]
theorem SuccOrder.nhds_bot {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [SuccOrder α] [OrderTopology α] [OrderBot α] :
nhds ⊥ = pure ⊥
source
@[simp]
theorem PredOrder.nhds_top {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [PredOrder α] [OrderTopology α] [OrderTop α] :
nhds ⊤ = pure ⊤
source
theorem SuccOrder.isOpen_iff {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [SuccOrder α] [OrderTopology α] {s : Set α} :
IsOpen s ↔ ∀ o ∈ s, Order.IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
source
theorem PredOrder.isOpen_iff {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [PredOrder α] [OrderTopology α] {s : Set α} :
IsOpen s ↔ ∀ o ∈ s, Order.IsPredLimit o → ∃ (a : α), o < a ∧ Set.Ioo o a ⊆ s
source
theorem SuccOrder.accPt_principal {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [SuccOrder α] [OrderTopology α] {a : α} {s : Set α} :
AccPt a (Filter.principal s) ↔ ¬IsMin a ∧ ∀ b < a, (s ∩ Set.Ioo b a).Nonempty
source
theorem PredOrder.accPt_principal {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [PredOrder α] [OrderTopology α] {a : α} {s : Set α} :
AccPt a (Filter.principal s) ↔ ¬IsMax a ∧ ∀ (b : α), a < b → (s ∩ Set.Ioo a b).Nonempty
source
theorem AccPt.not_isMin {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [SuccOrder α] [OrderTopology α] {a : α} {s : Set α} (h : AccPt a (Filter.principal s)) :
¬IsMin a
source
theorem AccPt.not_isMax {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [PredOrder α] [OrderTopology α] {a : α} {s : Set α} (h : AccPt a (Filter.principal s)) :
¬IsMax a
source
theorem AccPt.isSuccLimit {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [SuccOrder α] [OrderTopology α] {a : α} {s : Set α} (h : AccPt a (Filter.principal s)) :
Order.IsSuccLimit a
source
theorem AccPt.isPredLimit {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [PredOrder α] [OrderTopology α] {a : α} {s : Set α} (h : AccPt a (Filter.principal s)) :
Order.IsPredLimit a
source
theorem SuccOrder.isSuccLimit_of_mem_frontier {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [SuccOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : a ∈ frontier s) :
Order.IsSuccLimit a
source
theorem PredOrder.isPredLimit_of_mem_frontier {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [PredOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : a ∈ frontier s) :
Order.IsPredLimit a