# Theory of topology on ordered spaces #

## Main definitions #

The order topology on an ordered space is the topology generated by all open intervals (or equivalently by those of the form `(-∞, a)` and `(b, +∞)`). We define it as `Preorder.topology α`. However, we do not register it as an instance (as many existing ordered types already have topologies, which would be equal but not definitionally equal to `Preorder.topology α`). Instead, we introduce a class `OrderTopology α` (which is a `Prop`, also known as a mixin) saying that on the type `α` having already a topological space structure and a preorder structure, the topological structure is equal to the order topology.

We prove many basic properties of such topologies.

## Main statements #

This file contains the proofs of the following facts. For exact requirements (`OrderClosedTopology` vs `OrderTopology`, `Preorder` vs `PartialOrder` vs `LinearOrder` etc) see their statements.

- `exists_Ioc_subset_of_mem_nhds`, `exists_Ico_subset_of_mem_nhds` : if `x < y`, then any neighborhood of `x` includes an interval `[x, z)` for some `z ∈ (x, y]`, and any neighborhood of `y` includes an interval `(z, y]` for some `z ∈ [x, y)`.
- `tendsto_of_tendsto_of_tendsto_of_le_of_le` : theorem known as squeeze theorem, sandwich theorem, theorem of Carabinieri, and two policemen (and a drunk) theorem; if `g` and `h` both converge to `a`, and eventually `g x ≤ f x ≤ h x`, then `f` converges to `a`.

## Implementation notes #

We do not register the order topology as an instance on a preorder (or even on a linear order). Indeed, on many such spaces, a topology has already been constructed in a different way (think of the discrete spaces `ℕ` or `ℤ`, or `ℝ` that could inherit a topology as the completion of `ℚ`), and is in general not defeq to the one generated by the intervals. We make it available as a definition `Preorder.topology α` though, that can be registered as an instance when necessary, or for specific types.

source
class OrderTopology (α : Type u_1) [t : TopologicalSpace α] [Preorder α] :
Prop

The order topology on an ordered type is the topology generated by open intervals. We register it on a preorder, but it is mostly interesting in linear orders, where it is also order-closed. We define it as a mixin. If you want to introduce the order topology on a preorder, use `Preorder.topology`.

- topology_eq_generate_intervals : t = TopologicalSpace.generateFrom {s : Set α | ∃ (a : α), s = Set.Ioi a ∨ s = Set.Iio a}

  The topology is generated by open intervals `Set.Ioi _` and `Set.Iio _`.

Instances

source
def Preorder.topology (α : Type u_1) [Preorder α] :
TopologicalSpace α

(Order) topology on a partial order `α` generated by the subbase of open intervals `(a, ∞) = { x ∣ a < x }, (-∞, b) = {x ∣ x < b}` for all `a, b` in `α`. We do not register it as an instance as many ordered sets are already endowed with the same topology, most often in a non-defeq way though. Register as a local instance when necessary.

Equations

- Preorder.topology α = TopologicalSpace.generateFrom {s : Set α | ∃ (a : α), s = {b : α | a < b} ∨ s = {b : α | b < a}}

Instances For

source
instance instOrderTopologyOrderDual {α : Type u} [ts : TopologicalSpace α] [Preorder α] [t : OrderTopology α] :
OrderTopology α ᵒᵈ
source
theorem OrderTopology.continuous_iff {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] [TopologicalSpace β] {f : β → α} :
Continuous f ↔ ∀ (a : α), IsOpen (f ⁻¹' Set.Ioi a) ∧ IsOpen (f ⁻¹' Set.Iio a)
source
theorem isOpen_iff_generate_intervals {α : Type u} [ts : TopologicalSpace α] [Preorder α] [t : OrderTopology α] {s : Set α} :
IsOpen s ↔ TopologicalSpace.GenerateOpen {s : Set α | ∃ (a : α), s = Set.Ioi a ∨ s = Set.Iio a} s
source
theorem isOpen_lt' {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
IsOpen {b : α | a < b}
source
theorem isOpen_Ioi' {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
IsOpen (Set.Ioi a)
source
theorem isOpen_gt' {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
IsOpen {b : α | b < a}
source
theorem isOpen_Iio' {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
IsOpen (Set.Iio a)
source
theorem lt_mem_nhds {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {a b : α} (h : a < b) :
∀ᶠ (x : α) in nhds b, a < x
source
theorem le_mem_nhds {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {a b : α} (h : a < b) :
∀ᶠ (x : α) in nhds b, a ≤ x
source
theorem gt_mem_nhds {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {a b : α} (h : a < b) :
∀ᶠ (x : α) in nhds a, x < b
source
theorem ge_mem_nhds {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {a b : α} (h : a < b) :
∀ᶠ (x : α) in nhds a, x ≤ b
source
theorem nhds_eq_order {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
nhds a = (⨅ b ∈ Set.Iio a, Filter.principal (Set.Ioi b)) ⊓ ⨅ b ∈ Set.Ioi a, Filter.principal (Set.Iio b)
source
theorem tendsto_order {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {f : β → α} {a : α} {x : Filter β} :
Filter.Tendsto f x (nhds a) ↔ (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'
source
instance tendstoIccClassNhds {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
Filter.TendstoIxxClass Set.Icc (nhds a) (nhds a)
source
instance tendstoIcoClassNhds {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
Filter.TendstoIxxClass Set.Ico (nhds a) (nhds a)
source
instance tendstoIocClassNhds {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
Filter.TendstoIxxClass Set.Ioc (nhds a) (nhds a)
source
instance tendstoIooClassNhds {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
Filter.TendstoIxxClass Set.Ioo (nhds a) (nhds a)
source
theorem exists_countable_generateFrom_Ioi_Iio (α : Type u) [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] [SecondCountableTopology α] :
∃ (c : Set α), c.Countable ∧ ts = TopologicalSpace.generateFrom {s : Set α | ∃ a ∈ c, s = Set.Ioi a ∨ s = Set.Iio a}

In a second countable topological space with the order topology, the topology is generated by half-infinite open intervals with endpoints in a countable set.

source
theorem isTopologicalBasis_biInter_Ioi_Iio_of_generateFrom {α : Type u} [ts : TopologicalSpace α] [Preorder α] (c : Set α) (h : ts = TopologicalSpace.generateFrom {s : Set α | ∃ a ∈ c, s = Set.Ioi a ∨ s = Set.Iio a}) :
TopologicalSpace.IsTopologicalBasis {s : Set α | ∃ (f : Set α) (g : Set α), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Set.Ioi a) ∩ ⋂ a ∈ g, Set.Iio a}

If a topology is generated by half-open intervals with endpoints in a set `c`, then the sets formed by intersecting finitely many of these intervals form a topological basis.

source
theorem tendsto_of_tendsto_of_tendsto_of_le_of_le' {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α} (hg : Filter.Tendsto g b (nhds a)) (hh : Filter.Tendsto h b (nhds a)) (hgf : ∀ᶠ (b : β) in b, g b ≤ f b) (hfh : ∀ᶠ (b : β) in b, f b ≤ h b) :
Filter.Tendsto f b (nhds a)

Squeeze theorem (also known as sandwich theorem). This version assumes that inequalities hold eventually for the filter.

source
theorem Filter.Tendsto.squeeze' {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α} (hg : Tendsto g b (nhds a)) (hh : Tendsto h b (nhds a)) (hgf : ∀ᶠ (b : β) in b, g b ≤ f b) (hfh : ∀ᶠ (b : β) in b, f b ≤ h b) :
Tendsto f b (nhds a)

Alias of `tendsto_of_tendsto_of_tendsto_of_le_of_le'`.

Squeeze theorem (also known as sandwich theorem). This version assumes that inequalities hold eventually for the filter.

source
theorem tendsto_of_tendsto_of_tendsto_of_le_of_le {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α} (hg : Filter.Tendsto g b (nhds a)) (hh : Filter.Tendsto h b (nhds a)) (hgf : g ≤ f) (hfh : f ≤ h) :
Filter.Tendsto f b (nhds a)

Squeeze theorem (also known as sandwich theorem). This version assumes that inequalities hold everywhere.

source
theorem Filter.Tendsto.squeeze {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α} (hg : Tendsto g b (nhds a)) (hh : Tendsto h b (nhds a)) (hgf : g ≤ f) (hfh : f ≤ h) :
Tendsto f b (nhds a)

Alias of `tendsto_of_tendsto_of_tendsto_of_le_of_le`.

Squeeze theorem (also known as sandwich theorem). This version assumes that inequalities hold everywhere.

source
theorem nhds_order_unbounded {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (hu : ∃ (u : α), a < u) (hl : ∃ (l : α), l < a) :
nhds a = ⨅ (l : α), ⨅ (_ : l < a), ⨅ (u : α), ⨅ (_ : a < u), Filter.principal (Set.Ioo l u)
source
theorem tendsto_order_unbounded {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {f : β → α} {a : α} {x : Filter β} (hu : ∃ (u : α), a < u) (hl : ∃ (l : α), l < a) (h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u) :
Filter.Tendsto f x (nhds a)
source
instance tendstoIxxNhdsWithin {α : Type u_1} [TopologicalSpace α] (a : α) {s t : Set α} {Ixx : α → α → Set α} [Filter.TendstoIxxClass Ixx (nhds a) (nhds a)] [Filter.TendstoIxxClass Ixx (Filter.principal s) (Filter.principal t)] :
Filter.TendstoIxxClass Ixx (nhdsWithin a s) (nhdsWithin a t)
source
instance tendstoIccClassNhdsPi {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OrderTopology (α i)] (f : (i : ι) → α i) :
Filter.TendstoIxxClass Set.Icc (nhds f) (nhds f)
source
theorem induced_topology_le_preorder {α : Type u} {β : Type v} [Preorder α] [Preorder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : ∀ {x y : α}, f x < f y ↔ x < y) :
TopologicalSpace.induced f inst✝ ≤ Preorder.topology α
source
theorem induced_topology_eq_preorder {α : Type u} {β : Type v} [Preorder α] [Preorder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : ∀ {x y : α}, f x < f y ↔ x < y) (H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y) (H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b) :
TopologicalSpace.induced f inst✝ = Preorder.topology α
source
theorem induced_orderTopology' {α : Type u} {β : Type v} [Preorder α] [ta : TopologicalSpace β] [Preorder β] [OrderTopology β] (f : α → β) (hf : ∀ {x y : α}, f x < f y ↔ x < y) (H₁ : ∀ {a : α} {x : β}, x < f a → ∃ b < a, x ≤ f b) (H₂ : ∀ {a : α} {x : β}, f a < x → ∃ b > a, f b ≤ x) :
OrderTopology α
source
theorem induced_orderTopology {α : Type u} {β : Type v} [Preorder α] [ta : TopologicalSpace β] [Preorder β] [OrderTopology β] (f : α → β) (hf : ∀ {x y : α}, f x < f y ↔ x < y) (H : ∀ {x y : β}, x < y → ∃ (a : α), x < f a ∧ f a < y) :
OrderTopology α
source
theorem StrictMono.induced_topology_eq_preorder {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [t : TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : StrictMono f) (hc : (Set.range f).OrdConnected) :
TopologicalSpace.induced f t = Preorder.topology α

The topology induced by a strictly monotone function with order-connected range is the preorder topology.

source
theorem StrictMono.isEmbedding_of_ordConnected {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [TopologicalSpace α] [h : OrderTopology α] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : StrictMono f) (hc : (Set.range f).OrdConnected) :
Topology.IsEmbedding f

A strictly monotone function between linear orders with order topology is a topological embedding provided that the range of `f` is order-connected.

source
theorem OrderEmbedding.isEmbedding_of_ordConnected {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] [OrderTopology β] (f : α ↪o β) (hc : (Set.range ⇑f).OrdConnected) :
Topology.IsEmbedding ⇑f

An `OrderEmbedding` is a topological embedding provided that the range of `f` is order-connected

source
instance orderTopology_of_ordConnected {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α} [ht : t.OrdConnected] :
OrderTopology ↑t

On a `Set.OrdConnected` subset of a linear order, the order topology for the restriction of the order is the same as the restriction to the subset of the order topology.

source
theorem nhdsGE_eq_iInf_inf_principal {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
nhdsWithin a (Set.Ici a) = (⨅ (u : α), ⨅ (_ : a < u), Filter.principal (Set.Iio u)) ⊓ Filter.principal (Set.Ici a)
source
theorem nhdsLE_eq_iInf_inf_principal {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
nhdsWithin a (Set.Iic a) = (⨅ (l : α), ⨅ (_ : l < a), Filter.principal (Set.Ioi l)) ⊓ Filter.principal (Set.Iic a)
source
theorem nhdsGE_eq_iInf_principal {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (ha : ∃ (u : α), a < u) :
nhdsWithin a (Set.Ici a) = ⨅ (u : α), ⨅ (_ : a < u), Filter.principal (Set.Ico a u)
source
theorem nhdsLE_eq_iInf_principal {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (ha : ∃ (l : α), l < a) :
nhdsWithin a (Set.Iic a) = ⨅ (l : α), ⨅ (_ : l < a), Filter.principal (Set.Ioc l a)
source
theorem nhdsGE_basis_of_exists_gt {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : ∃ (u : α), a < u) :
(nhdsWithin a (Set.Ici a)).HasBasis (fun (u : α) => a < u) fun (u : α) => Set.Ico a u
source
theorem nhdsLE_basis_of_exists_lt {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : ∃ (l : α), l < a) :
(nhdsWithin a (Set.Iic a)).HasBasis (fun (l : α) => l < a) fun (l : α) => Set.Ioc l a
source
theorem nhdsGE_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) :
(nhdsWithin a (Set.Ici a)).HasBasis (fun (u : α) => a < u) fun (u : α) => Set.Ico a u
source
theorem nhdsLE_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] (a : α) :
(nhdsWithin a (Set.Iic a)).HasBasis (fun (l : α) => l < a) fun (l : α) => Set.Ioc l a
source
theorem nhds_top_order {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTop α] [OrderTopology α] :
nhds ⊤ = ⨅ (l : α), ⨅ (_ : l < ⊤), Filter.principal (Set.Ioi l)
source
theorem nhds_bot_order {α : Type u} [TopologicalSpace α] [Preorder α] [OrderBot α] [OrderTopology α] :
nhds ⊥ = ⨅ (l : α), ⨅ (_ : ⊥ < l), Filter.principal (Set.Iio l)
source
theorem nhds_top_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] [Nontrivial α] :
(nhds ⊤).HasBasis (fun (a : α) => a < ⊤) fun (a : α) => Set.Ioi a
source
theorem nhds_bot_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] [Nontrivial α] :
(nhds ⊥).HasBasis (fun (a : α) => ⊥ < a) fun (a : α) => Set.Iio a
source
theorem nhds_top_basis_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] [Nontrivial α] [DenselyOrdered α] :
(nhds ⊤).HasBasis (fun (a : α) => a < ⊤) Set.Ici
source
theorem nhds_bot_basis_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] [Nontrivial α] [DenselyOrdered α] :
(nhds ⊥).HasBasis (fun (a : α) => ⊥ < a) Set.Iic
source
theorem tendsto_nhds_top_mono {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] {l : Filter α} {f g : α → β} (hf : Filter.Tendsto f l (nhds ⊤)) (hg : f ≤ᶠ[l] g) :
Filter.Tendsto g l (nhds ⊤)
source
theorem tendsto_nhds_bot_mono {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β] {l : Filter α} {f g : α → β} (hf : Filter.Tendsto f l (nhds ⊥)) (hg : g ≤ᶠ[l] f) :
Filter.Tendsto g l (nhds ⊥)
source
theorem tendsto_nhds_top_mono' {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] {l : Filter α} {f g : α → β} (hf : Filter.Tendsto f l (nhds ⊤)) (hg : f ≤ g) :
Filter.Tendsto g l (nhds ⊤)
source
theorem tendsto_nhds_bot_mono' {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β] {l : Filter α} {f g : α → β} (hf : Filter.Tendsto f l (nhds ⊥)) (hg : g ≤ f) :
Filter.Tendsto g l (nhds ⊥)
source
theorem order_separated {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a₁ a₂ : α} (h : a₁ < a₂) :
∃ (u : Set α) (v : Set α), IsOpen u ∧ IsOpen v ∧ a₁ ∈ u ∧ a₂ ∈ v ∧ ∀ b₁ ∈ u, ∀ b₂ ∈ v, b₁ < b₂
source
@[instance 100]
instance OrderTopology.to_orderClosedTopology {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] :
OrderClosedTopology α
source
theorem exists_Ioc_subset_of_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ nhds a) (h : ∃ (l : α), l < a) :
∃ l < a, Set.Ioc l a ⊆ s
source
theorem exists_Ioc_subset_of_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ nhds a) {l : α} (hl : l < a) :
∃ l' ∈ Set.Ico l a, Set.Ioc l' a ⊆ s
source
theorem exists_Ico_subset_of_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ nhds a) {u : α} (hu : a < u) :
∃ u' ∈ Set.Ioc a u, Set.Ico a u' ⊆ s
source
theorem exists_Ico_subset_of_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ nhds a) (h : ∃ (u : α), a < u) :
∃ (u : α), a < u ∧ Set.Ico a u ⊆ s
source
theorem exists_Icc_mem_subset_of_mem_nhdsGE {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ nhdsWithin a (Set.Ici a)) :
∃ (b : α), a ≤ b ∧ Set.Icc a b ∈ nhdsWithin a (Set.Ici a) ∧ Set.Icc a b ⊆ s
source
theorem exists_Icc_mem_subset_of_mem_nhdsLE {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ nhdsWithin a (Set.Iic a)) :
∃ b ≤ a, Set.Icc b a ∈ nhdsWithin a (Set.Iic a) ∧ Set.Icc b a ⊆ s
source
theorem exists_Icc_mem_subset_of_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ nhds a) :
∃ (b : α) (c : α), a ∈ Set.Icc b c ∧ Set.Icc b c ∈ nhds a ∧ Set.Icc b c ⊆ s
source
theorem IsOpen.exists_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Nontrivial α] {s : Set α} (hs : IsOpen s) (h : s.Nonempty) :
∃ (a : α) (b : α), a < b ∧ Set.Ioo a b ⊆ s
source
theorem dense_of_exists_between {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Nontrivial α] {s : Set α} (h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, a < c ∧ c < b) :
Dense s
source
theorem IsUpperSet.isClosed {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [WellFoundedLT α] {s : Set α} (h : IsUpperSet s) :
IsClosed s
source
theorem IsLowerSet.isClosed {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [WellFoundedGT α] {s : Set α} (h : IsLowerSet s) :
IsClosed s
source
theorem IsLowerSet.isOpen {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [WellFoundedLT α] {s : Set α} (h : IsLowerSet s) :
IsOpen s
source
theorem IsUpperSet.isOpen {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [WellFoundedGT α] {s : Set α} (h : IsUpperSet s) :
IsOpen s
source
theorem dense_iff_exists_between {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [Nontrivial α] {s : Set α} :
Dense s ↔ ∀ (a b : α), a < b → ∃ c ∈ s, a < c ∧ c < b

A set in a nontrivial densely linear ordered type is dense in the sense of topology if and only if for any `a < b` there exists `c ∈ s`, `a < c < b`. Each implication requires less typeclass assumptions.

source
theorem mem_nhds_iff_exists_Ioo_subset' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hl : ∃ (l : α), l < a) (hu : ∃ (u : α), a < u) :
s ∈ nhds a ↔ ∃ (l : α) (u : α), a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ s

A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`, provided `a` is neither a bottom element nor a top element.

source
theorem mem_nhds_iff_exists_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α} {s : Set α} :
s ∈ nhds a ↔ ∃ (l : α) (u : α), a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ s

A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`.

source
theorem nhds_basis_Ioo' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (hl : ∃ (l : α), l < a) (hu : ∃ (u : α), a < u) :
(nhds a).HasBasis (fun (b : α × α) => b.1 < a ∧ a < b.2) fun (b : α × α) => Set.Ioo b.1 b.2
source
theorem nhds_basis_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] (a : α) :
(nhds a).HasBasis (fun (b : α × α) => b.1 < a ∧ a < b.2) fun (b : α × α) => Set.Ioo b.1 b.2
source
theorem Filter.Eventually.exists_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α} {p : α → Prop} (hp : ∀ᶠ (x : α) in nhds a, p x) :
∃ (l : α) (u : α), a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ {x : α | p x}
source
theorem Dense.topology_eq_generateFrom {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) :
inst✝ = TopologicalSpace.generateFrom (Set.Ioi '' s ∪ Set.Iio '' s)
source
theorem PredOrder.hasBasis_nhds_Ioc_of_exists_gt {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [PredOrder α] {a : α} (ha : ∃ (u : α), a < u) :
(nhds a).HasBasis (fun (x : α) => a < x) fun (x : α) => Set.Ico a x
source
theorem PredOrder.hasBasis_nhds_Ioc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [PredOrder α] [NoMaxOrder α] {a : α} :
(nhds a).HasBasis (fun (x : α) => a < x) fun (x : α) => Set.Ico a x
source
theorem SuccOrder.hasBasis_nhds_Ioc_of_exists_lt {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SuccOrder α] {a : α} (ha : ∃ (l : α), l < a) :
(nhds a).HasBasis (fun (x : α) => x < a) fun (x : α) => Set.Ioc x a
source
theorem SuccOrder.hasBasis_nhds_Ioc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SuccOrder α] {a : α} [NoMinOrder α] :
(nhds a).HasBasis (fun (x : α) => x < a) fun (x : α) => Set.Ioc x a
source
theorem SecondCountableTopology.of_separableSpace_orderTopology (α : Type u) [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [TopologicalSpace.SeparableSpace α] :
SecondCountableTopology α

Let `α` be a densely ordered linear order with order topology. If `α` is a separable space, then it has second countable topology. Note that the "densely ordered" assumption cannot be dropped, see double arrow space for a counterexample.

source
theorem countable_setOf_covBy_right {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] :
{x : α | ∃ (y : α), x ⋖ y}.Countable

The set of points which are isolated on the right is countable when the space is second-countable.

source
theorem countable_setOf_covBy_left {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] :
{x : α | ∃ (y : α), y ⋖ x}.Countable

The set of points which are isolated on the left is countable when the space is second-countable.

source
theorem countable_of_isolated_left' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] :
{x : α | ∃ y < x, Set.Ioo y x = ∅}.Countable

The set of points which are isolated on the left is countable when the space is second-countable.

source
theorem Set.PairwiseDisjoint.countable_of_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {y : α → α} {s : Set α} (h : s.PairwiseDisjoint fun (x : α) => Ioo x (y x)) (h' : ∀ x ∈ s, x < y x) :
s.Countable

Consider a disjoint family of intervals `(x, y)` with `x < y` in a second-countable space. Then the family is countable. This is not a straightforward consequence of second-countability as some of these intervals might be empty (but in fact this can happen only for countably many of them).

source
theorem countable_image_lt_image_Ioi_within {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] [SecondCountableTopology α] (t : Set β) (f : β → α) :
{x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}.Countable

For a function taking values in a second countable space, the set of points `x` for which the image under `f` of `(x, ∞)` is separated above from `f x` is countable. We give here a version relative to a set `t`.

source
theorem countable_image_lt_image_Ioi {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] :
{x : β | ∃ (z : α), f x < z ∧ ∀ (y : β), x < y → z ≤ f y}.Countable

For a function taking values in a second countable space, the set of points `x` for which the image under `f` of `(x, ∞)` is separated above from `f x` is countable.

source
theorem countable_image_gt_image_Ioi_within {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] [SecondCountableTopology α] (t : Set β) (f : β → α) :
{x : β | x ∈ t ∧ ∃ z < f x, ∀ y ∈ t, x < y → f y ≤ z}.Countable

For a function taking values in a second countable space, the set of points `x` for which the image under `f` of `(x, ∞)` is separated below from `f x` is countable. We give here a version relative to a set `t`.

source
theorem countable_image_gt_image_Ioi {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] :
{x : β | ∃ z < f x, ∀ (y : β), x < y → f y ≤ z}.Countable

For a function taking values in a second countable space, the set of points `x` for which the image under `f` of `(x, ∞)` is separated below from `f x` is countable.

source
theorem countable_image_lt_image_Iio_within {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] [SecondCountableTopology α] (t : Set β) (f : β → α) :
{x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, y < x → z ≤ f y}.Countable

For a function taking values in a second countable space, the set of points `x` for which the image under `f` of `(-∞, x)` is separated above from `f x` is countable. We give here a version relative to a set `t`.

source
theorem countable_image_lt_image_Iio {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] :
{x : β | ∃ (z : α), f x < z ∧ ∀ y < x, z ≤ f y}.Countable

For a function taking values in a second countable space, the set of points `x` for which the image under `f` of `(-∞, x)` is separated above from `f x` is countable.

source
theorem countable_image_gt_image_Iio_within {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] [SecondCountableTopology α] (t : Set β) (f : β → α) :
{x : β | x ∈ t ∧ ∃ z < f x, ∀ y ∈ t, y < x → f y ≤ z}.Countable

For a function taking values in a second countable space, the set of points `x` for which the image under `f` of `(-∞, x)` is separated below from `f x` is countable. We give here a version relative to a set `t`.

source
theorem countable_image_gt_image_Iio {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] :
{x : β | ∃ z < f x, ∀ y < x, f y ≤ z}.Countable

For a function taking values in a second countable space, the set of points `x` for which the image under `f` of `(-∞, x)` is separated below from `f x` is countable.

source
instance instIsCountablyGenerated_atTop {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] :
Filter.atTop.IsCountablyGenerated
source
instance instIsCountablyGenerated_atBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] :
Filter.atBot.IsCountablyGenerated

### Intervals in `Π i, X i` belong to `𝓝 x` #

For each lemma `pi_Ixx_mem_nhds` we add a non-dependent version `pi_Ixx_mem_nhds'` because sometimes Lean fails to unify different instances while trying to apply the dependent version to, e.g., `ι → ℝ`.

source
theorem pi_Iic_mem_nhds {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a x : (i : ι) → X i} (ha : ∀ (i : ι), x i < a i) :
Set.Iic a ∈ nhds x
source
theorem pi_Iic_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' x' : ι → α} (ha : ∀ (i : ι), x' i < a' i) :
Set.Iic a' ∈ nhds x'
source
theorem pi_Ici_mem_nhds {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a x : (i : ι) → X i} (ha : ∀ (i : ι), a i < x i) :
Set.Ici a ∈ nhds x
source
theorem pi_Ici_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' x' : ι → α} (ha : ∀ (i : ι), a' i < x' i) :
Set.Ici a' ∈ nhds x'
source
theorem pi_Icc_mem_nhds {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a b x : (i : ι) → X i} (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
Set.Icc a b ∈ nhds x
source
theorem pi_Icc_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' b' x' : ι → α} (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
Set.Icc a' b' ∈ nhds x'
source
theorem pi_Iio_mem_nhds {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a x : (i : ι) → X i} [Nonempty ι] (ha : ∀ (i : ι), x i < a i) :
Set.Iio a ∈ nhds x
source
theorem pi_Iio_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' x' : ι → α} [Nonempty ι] (ha : ∀ (i : ι), x' i < a' i) :
Set.Iio a' ∈ nhds x'
source
theorem pi_Ioi_mem_nhds {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a x : (i : ι) → X i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) :
Set.Ioi a ∈ nhds x
source
theorem pi_Ioi_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' x' : ι → α} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) :
Set.Ioi a' ∈ nhds x'
source
theorem pi_Ioc_mem_nhds {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a b x : (i : ι) → X i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
Set.Ioc a b ∈ nhds x
source
theorem pi_Ioc_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' b' x' : ι → α} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
Set.Ioc a' b' ∈ nhds x'
source
theorem pi_Ico_mem_nhds {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a b x : (i : ι) → X i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
Set.Ico a b ∈ nhds x
source
theorem pi_Ico_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' b' x' : ι → α} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
Set.Ico a' b' ∈ nhds x'
source
theorem pi_Ioo_mem_nhds {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a b x : (i : ι) → X i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
Set.Ioo a b ∈ nhds x
source
theorem pi_Ioo_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' b' x' : ι → α} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
Set.Ioo a' b' ∈ nhds x'
source
theorem LeftOrdContinuous.continuousWithinAt_Iic {X : Type u_1} [ConditionallyCompleteLinearOrder X] [TopologicalSpace X] [OrderTopology X] {Y : Type u_2} [ConditionallyCompleteLinearOrder Y] [TopologicalSpace Y] [OrderTopology Y] [DenselyOrdered X] {f : X → Y} {x : X} (hf : LeftOrdContinuous f) :
ContinuousWithinAt f (Set.Iic x) x

An order-theoretically left-continuous function is topologically left-continuous, assuming the function is between conditionally complete linear orders with order topologies, and the domain is densely ordered.

source
theorem RightOrdContinuous.continuousWithinAt_Ici {X : Type u_1} [ConditionallyCompleteLinearOrder X] [TopologicalSpace X] [OrderTopology X] {Y : Type u_2} [ConditionallyCompleteLinearOrder Y] [TopologicalSpace Y] [OrderTopology Y] [DenselyOrdered X] {f : X → Y} {x : X} (hf : RightOrdContinuous f) :
ContinuousWithinAt f (Set.Ici x) x

An order-theoretically right-continuous function is topologically right-continuous, assuming the function is between conditionally complete linear orders with order topologies, and the domain is densely ordered.