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.

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 _.

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}}

instance instOrderTopologyOrderDualInstTopologicalSpaceOrderDualInstPreorder {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] : OrderTopology αᵒᵈ

Equations

• ⋯ = ⋯

theorem isOpen_iff_generate_intervals {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {s : Set α} : IsOpen s ↔ TopologicalSpace.GenerateOpen {s : Set α | ∃ (a : α), s = Set.Ioi a ∨ s = Set.Iio a} s

theorem isOpen_lt' {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] (a : α) : IsOpen {b : α | a < b}

theorem isOpen_gt' {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] (a : α) : IsOpen {b : α | b < a}

theorem lt_mem_nhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {a : α} {b : α} (h : a < b) : ∀ᶠ (x : α) in nhds b, a < x

theorem le_mem_nhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {a : α} {b : α} (h : a < b) : ∀ᶠ (x : α) in nhds b, a ≤ x

theorem gt_mem_nhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {a : α} {b : α} (h : a < b) : ∀ᶠ (x : α) in nhds a, x < b

theorem ge_mem_nhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {a : α} {b : α} (h : a < b) : ∀ᶠ (x : α) in nhds a, x ≤ b

theorem nhds_eq_order {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] (a : α) : nhds a = (⨅ b ∈ Set.Iio a, Filter.principal (Set.Ioi b)) ⊓ ⨅ b ∈ Set.Ioi a, Filter.principal (Set.Iio b)

theorem tendsto_order {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : 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'

instance tendstoIccClassNhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] (a : α) : Filter.TendstoIxxClass Set.Icc (nhds a) (nhds a)

Equations

• ⋯ = ⋯

instance tendstoIcoClassNhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] (a : α) : Filter.TendstoIxxClass Set.Ico (nhds a) (nhds a)

Equations

• ⋯ = ⋯

instance tendstoIocClassNhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] (a : α) : Filter.TendstoIxxClass Set.Ioc (nhds a) (nhds a)

Equations

• ⋯ = ⋯

instance tendstoIooClassNhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] (a : α) : Filter.TendstoIxxClass Set.Ioo (nhds a) (nhds a)

Equations

• ⋯ = ⋯

theorem tendsto_of_tendsto_of_tendsto_of_le_of_le' {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : 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.

theorem tendsto_of_tendsto_of_tendsto_of_le_of_le {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : 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.

theorem nhds_order_unbounded {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {a : α} (hu : ∃ (u : α), a < u) (hl : ∃ (l : α), l < a) : nhds a = ⨅ (l : α), ⨅ (_ : l < a), ⨅ (u : α), ⨅ (_ : a < u), Filter.principal (Set.Ioo l u)

theorem tendsto_order_unbounded {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : 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)

instance tendstoIxxNhdsWithin {α : Type u_1} [TopologicalSpace α] (a : α) {s : Set α} {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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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 α

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 α

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 α

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 α

theorem StrictMono.induced_topology_eq_preorder {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [t : TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : StrictMono f) (hc : Set.OrdConnected (Set.range f)) : TopologicalSpace.induced f t = Preorder.topology α

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

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

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

instance orderTopology_of_ordConnected {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α} [ht : Set.OrdConnected t] : 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.

Equations

• ⋯ = ⋯

theorem nhdsWithin_Ici_eq'' {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : nhdsWithin a (Set.Ici a) = (⨅ (u : α), ⨅ (_ : a < u), Filter.principal (Set.Iio u)) ⊓ Filter.principal (Set.Ici a)

theorem nhdsWithin_Iic_eq'' {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : nhdsWithin a (Set.Iic a) = (⨅ (l : α), ⨅ (_ : l < a), Filter.principal (Set.Ioi l)) ⊓ Filter.principal (Set.Iic a)

theorem nhdsWithin_Ici_eq' {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (ha : ∃ (u : α), a < u) : nhdsWithin a (Set.Ici a) = ⨅ (u : α), ⨅ (_ : a < u), Filter.principal (Set.Ico a u)

theorem nhdsWithin_Iic_eq' {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (ha : ∃ (l : α), l < a) : nhdsWithin a (Set.Iic a) = ⨅ (l : α), ⨅ (_ : l < a), Filter.principal (Set.Ioc l a)

theorem nhdsWithin_Ici_basis' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : ∃ (u : α), a < u) : Filter.HasBasis (nhdsWithin a (Set.Ici a)) (fun (u : α) => a < u) fun (u : α) => Set.Ico a u

theorem nhdsWithin_Iic_basis' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : ∃ (l : α), l < a) : Filter.HasBasis (nhdsWithin a (Set.Iic a)) (fun (l : α) => l < a) fun (l : α) => Set.Ioc l a

theorem nhdsWithin_Ici_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) : Filter.HasBasis (nhdsWithin a (Set.Ici a)) (fun (u : α) => a < u) fun (u : α) => Set.Ico a u

theorem nhdsWithin_Iic_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] (a : α) : Filter.HasBasis (nhdsWithin a (Set.Iic a)) (fun (l : α) => l < a) fun (l : α) => Set.Ioc l a

theorem nhds_top_order {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTop α] [OrderTopology α] : nhds ⊤ = ⨅ (l : α), ⨅ (_ : l < ⊤), Filter.principal (Set.Ioi l)

theorem nhds_bot_order {α : Type u} [TopologicalSpace α] [Preorder α] [OrderBot α] [OrderTopology α] : nhds ⊥ = ⨅ (l : α), ⨅ (_ : ⊥ < l), Filter.principal (Set.Iio l)

theorem nhds_top_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] [Nontrivial α] : Filter.HasBasis (nhds ⊤) (fun (a : α) => a < ⊤) fun (a : α) => Set.Ioi a

theorem nhds_bot_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] [Nontrivial α] : Filter.HasBasis (nhds ⊥) (fun (a : α) => ⊥ < a) fun (a : α) => Set.Iio a

theorem nhds_top_basis_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] [Nontrivial α] [DenselyOrdered α] : Filter.HasBasis (nhds ⊤) (fun (a : α) => a < ⊤) Set.Ici

theorem nhds_bot_basis_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] [Nontrivial α] [DenselyOrdered α] : Filter.HasBasis (nhds ⊥) (fun (a : α) => ⊥ < a) Set.Iic

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 ⊤)

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 ⊥)

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 ⊤)

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 ⊥)

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₂

instance OrderTopology.to_orderClosedTopology {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] : OrderClosedTopology α

Equations

• ⋯ = ⋯

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

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

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

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

theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Ici {α : 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

theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Iic {α : 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

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

theorem IsOpen.exists_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Nontrivial α] {s : Set α} (hs : IsOpen s) (h : Set.Nonempty s) : ∃ (a : α) (b : α), a < b ∧ Set.Ioo a b ⊆ s

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

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.

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.

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.

theorem nhds_basis_Ioo' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (hl : ∃ (l : α), l < a) (hu : ∃ (u : α), a < u) : Filter.HasBasis (nhds a) (fun (b : α × α) => b.1 < a ∧ a < b.2) fun (b : α × α) => Set.Ioo b.1 b.2

theorem nhds_basis_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] (a : α) : Filter.HasBasis (nhds a) (fun (b : α × α) => b.1 < a ∧ a < b.2) fun (b : α × α) => Set.Ioo b.1 b.2

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}

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)

@[deprecated Filter.OrderBot.atBot_eq]

theorem atBot_le_nhds_bot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderBot α] : Filter.atBot ≤ nhds ⊥

@[deprecated Filter.OrderTop.atTop_eq]

theorem atTop_le_nhds_top {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTop α] : Filter.atTop ≤ nhds ⊤

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.

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

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

@[deprecated countable_setOf_covBy_right]

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

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

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

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

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

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

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

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).

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

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.

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

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.

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

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.

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

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.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

Intervals in Π i, π 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., ι → ℝ.

theorem pi_Iic_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {x : (i : ι) → π i} (ha : ∀ (i : ι), x i < a i) : Set.Iic a ∈ nhds x

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'

theorem pi_Ici_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {x : (i : ι) → π i} (ha : ∀ (i : ι), a i < x i) : Set.Ici a ∈ nhds x

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'

theorem pi_Icc_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {x : (i : ι) → π i} (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) : Set.Icc a b ∈ nhds x

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'

theorem pi_Iio_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), x i < a i) : Set.Iio a ∈ nhds x

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'

theorem pi_Ioi_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) : Set.Ioi a ∈ nhds x

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'

theorem pi_Ioc_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) : Set.Ioc a b ∈ nhds x

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'

theorem pi_Ico_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) : Set.Ico a b ∈ nhds x

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'

theorem pi_Ioo_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) : Set.Ioo a b ∈ nhds x

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'

Neighborhoods to the left and to the right on an OrderTopology

We've seen some properties of left and right neighborhood of a point in an OrderClosedTopology. In an OrderTopology, such neighborhoods can be characterized as the sets containing suitable intervals to the right or to the left of a. We give now these characterizations.

theorem TFAE_mem_nhdsWithin_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {b : α} (hab : a < b) (s : Set α) : List.TFAE [s ∈ nhdsWithin a (Set.Ioi a), s ∈ nhdsWithin a (Set.Ioc a b), s ∈ nhdsWithin a (Set.Ioo a b), ∃ u ∈ Set.Ioc a b, Set.Ioo a u ⊆ s, ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s]

The following statements are equivalent:

0. s is a neighborhood of a within (a, +∞);
1. s is a neighborhood of a within (a, b];
2. s is a neighborhood of a within (a, b);
3. s includes (a, u) for some u ∈ (a, b];
4. s includes (a, u) for some u > a.

theorem mem_nhdsWithin_Ioi_iff_exists_mem_Ioc_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {u' : α} {s : Set α} (hu' : a < u') : s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioc a u', Set.Ioo a u ⊆ s

theorem mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {u' : α} {s : Set α} (hu' : a < u') : s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s

A set is a neighborhood of a within (a, +∞) if and only if it contains an interval (a, u) with a < u < u', provided a is not a top element.

theorem nhdsWithin_Ioi_basis' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (h : ∃ (b : α), a < b) : Filter.HasBasis (nhdsWithin a (Set.Ioi a)) (fun (x : α) => a < x) (Set.Ioo a)

theorem nhdsWithin_Ioi_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) : Filter.HasBasis (nhdsWithin a (Set.Ioi a)) (fun (x : α) => a < x) (Set.Ioo a)

theorem nhdsWithin_Ioi_eq_bot_iff {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} : nhdsWithin a (Set.Ioi a) = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b

theorem mem_nhdsWithin_Ioi_iff_exists_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s

A set is a neighborhood of a within (a, +∞) if and only if it contains an interval (a, u) with a < u.

theorem countable_setOf_isolated_right {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] : Set.Countable {x : α | nhdsWithin x (Set.Ioi x) = ⊥}

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

theorem countable_setOf_isolated_left {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] : Set.Countable {x : α | nhdsWithin x (Set.Iio x) = ⊥}

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

theorem mem_nhdsWithin_Ioi_iff_exists_Ioc_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioc a u ⊆ s

A set is a neighborhood of a within (a, +∞) if and only if it contains an interval (a, u] with a < u.

theorem TFAE_mem_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {b : α} (h : a < b) (s : Set α) : List.TFAE [s ∈ nhdsWithin b (Set.Iio b), s ∈ nhdsWithin b (Set.Ico a b), s ∈ nhdsWithin b (Set.Ioo a b), ∃ l ∈ Set.Ico a b, Set.Ioo l b ⊆ s, ∃ l ∈ Set.Iio b, Set.Ioo l b ⊆ s]

The following statements are equivalent:

0. s is a neighborhood of b within (-∞, b)
1. s is a neighborhood of b within [a, b)
2. s is a neighborhood of b within (a, b)
3. s includes (l, b) for some l ∈ [a, b)
4. s includes (l, b) for some l < b

theorem mem_nhdsWithin_Iio_iff_exists_mem_Ico_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {l' : α} {s : Set α} (hl' : l' < a) : s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Ico l' a, Set.Ioo l a ⊆ s

theorem mem_nhdsWithin_Iio_iff_exists_Ioo_subset' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {l' : α} {s : Set α} (hl' : l' < a) : s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ioo l a ⊆ s

A set is a neighborhood of a within (-∞, a) if and only if it contains an interval (l, a) with l < a, provided a is not a bottom element.

theorem mem_nhdsWithin_Iio_iff_exists_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ioo l a ⊆ s

A set is a neighborhood of a within (-∞, a) if and only if it contains an interval (l, a) with l < a.

theorem mem_nhdsWithin_Iio_iff_exists_Ico_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ico l a ⊆ s

A set is a neighborhood of a within (-∞, a) if and only if it contains an interval [l, a) with l < a.

theorem nhdsWithin_Iio_basis' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (h : ∃ (b : α), b < a) : Filter.HasBasis (nhdsWithin a (Set.Iio a)) (fun (x : α) => x < a) fun (x : α) => Set.Ioo x a

theorem nhdsWithin_Iio_eq_bot_iff {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} : nhdsWithin a (Set.Iio a) = ⊥ ↔ IsBot a ∨ ∃ (b : α), b ⋖ a

theorem TFAE_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {b : α} (hab : a < b) (s : Set α) : List.TFAE [s ∈ nhdsWithin a (Set.Ici a), s ∈ nhdsWithin a (Set.Icc a b), s ∈ nhdsWithin a (Set.Ico a b), ∃ u ∈ Set.Ioc a b, Set.Ico a u ⊆ s, ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s]

The following statements are equivalent:

0. s is a neighborhood of a within [a, +∞);
1. s is a neighborhood of a within [a, b];
2. s is a neighborhood of a within [a, b);
3. s includes [a, u) for some u ∈ (a, b];
4. s includes [a, u) for some u > a.

theorem mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {u' : α} {s : Set α} (hu' : a < u') : s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u ∈ Set.Ioc a u', Set.Ico a u ⊆ s

theorem mem_nhdsWithin_Ici_iff_exists_Ico_subset' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {u' : α} {s : Set α} (hu' : a < u') : s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s

A set is a neighborhood of a within [a, +∞) if and only if it contains an interval [a, u) with a < u < u', provided a is not a top element.

theorem mem_nhdsWithin_Ici_iff_exists_Ico_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s

A set is a neighborhood of a within [a, +∞) if and only if it contains an interval [a, u) with a < u.

theorem nhdsWithin_Ici_basis_Ico {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) : Filter.HasBasis (nhdsWithin a (Set.Ici a)) (fun (u : α) => a < u) (Set.Ico a)

theorem nhdsWithin_Ici_basis_Icc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] {a : α} : Filter.HasBasis (nhdsWithin a (Set.Ici a)) (fun (x : α) => a < x) (Set.Icc a)

The filter of right neighborhoods has a basis of closed intervals.

theorem mem_nhdsWithin_Ici_iff_exists_Icc_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ (u : α), a < u ∧ Set.Icc a u ⊆ s

A set is a neighborhood of a within [a, +∞) if and only if it contains an interval [a, u] with a < u.

theorem TFAE_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {b : α} (h : a < b) (s : Set α) : List.TFAE [s ∈ nhdsWithin b (Set.Iic b), s ∈ nhdsWithin b (Set.Icc a b), s ∈ nhdsWithin b (Set.Ioc a b), ∃ l ∈ Set.Ico a b, Set.Ioc l b ⊆ s, ∃ l ∈ Set.Iio b, Set.Ioc l b ⊆ s]

The following statements are equivalent:

0. s is a neighborhood of b within (-∞, b]
1. s is a neighborhood of b within [a, b]
2. s is a neighborhood of b within (a, b]
3. s includes (l, b] for some l ∈ [a, b)
4. s includes (l, b] for some l < b

theorem mem_nhdsWithin_Iic_iff_exists_mem_Ico_Ioc_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {l' : α} {s : Set α} (hl' : l' < a) : s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l ∈ Set.Ico l' a, Set.Ioc l a ⊆ s

theorem mem_nhdsWithin_Iic_iff_exists_Ioc_subset' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {l' : α} {s : Set α} (hl' : l' < a) : s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l ∈ Set.Iio a, Set.Ioc l a ⊆ s

A set is a neighborhood of a within (-∞, a] if and only if it contains an interval (l, a] with l < a, provided a is not a bottom element.

theorem mem_nhdsWithin_Iic_iff_exists_Ioc_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l ∈ Set.Iio a, Set.Ioc l a ⊆ s

A set is a neighborhood of a within (-∞, a] if and only if it contains an interval (l, a] with l < a.

theorem mem_nhdsWithin_Iic_iff_exists_Icc_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l < a, Set.Icc l a ⊆ s

A set is a neighborhood of a within (-∞, a] if and only if it contains an interval [l, a] with l < a.

theorem nhdsWithin_Iic_basis_Icc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] [DenselyOrdered α] {a : α} : Filter.HasBasis (nhdsWithin a (Set.Iic a)) (fun (x : α) => x < a) fun (x : α) => Set.Icc x a

The filter of left neighborhoods has a basis of closed intervals.

theorem nhds_eq_iInf_abs_sub {α : Type u} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] (a : α) : nhds a = ⨅ (r : α), ⨅ (_ : r > 0), Filter.principal {b : α | |a - b| < r}

theorem orderTopology_of_nhds_abs {α : Type u_1} [TopologicalSpace α] [LinearOrderedAddCommGroup α] (h_nhds : ∀ (a : α), nhds a = ⨅ (r : α), ⨅ (_ : r > 0), Filter.principal {b : α | |a - b| < r}) : OrderTopology α

theorem LinearOrderedAddCommGroup.tendsto_nhds {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {f : β → α} {x : Filter β} {a : α} : Filter.Tendsto f x (nhds a) ↔ ∀ ε > 0, ∀ᶠ (b : β) in x, |f b - a| < ε

theorem eventually_abs_sub_lt {α : Type u} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] (a : α) {ε : α} (hε : 0 < ε) : ∀ᶠ (x : α) in nhds a, |x - a| < ε

theorem Filter.Tendsto.add_atTop {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {l : Filter β} {f : β → α} {g : β → α} {C : α} (hf : Filter.Tendsto f l (nhds C)) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun (x : β) => f x + g x) l Filter.atTop

In a linearly ordered additive commutative group with the order topology, if f tends to C and g tends to atTop then f + g tends to atTop.

theorem Filter.Tendsto.add_atBot {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {l : Filter β} {f : β → α} {g : β → α} {C : α} (hf : Filter.Tendsto f l (nhds C)) (hg : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun (x : β) => f x + g x) l Filter.atBot

In a linearly ordered additive commutative group with the order topology, if f tends to C and g tends to atBot then f + g tends to atBot.

theorem Filter.Tendsto.atTop_add {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {l : Filter β} {f : β → α} {g : β → α} {C : α} (hf : Filter.Tendsto f l Filter.atTop) (hg : Filter.Tendsto g l (nhds C)) : Filter.Tendsto (fun (x : β) => f x + g x) l Filter.atTop

In a linearly ordered additive commutative group with the order topology, if f tends to atTop and g tends to C then f + g tends to atTop.

theorem Filter.Tendsto.atBot_add {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {l : Filter β} {f : β → α} {g : β → α} {C : α} (hf : Filter.Tendsto f l Filter.atBot) (hg : Filter.Tendsto g l (nhds C)) : Filter.Tendsto (fun (x : β) => f x + g x) l Filter.atBot

In a linearly ordered additive commutative group with the order topology, if f tends to atBot and g tends to C then f + g tends to atBot.

theorem nhds_basis_abs_sub_lt {α : Type u} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] (a : α) : Filter.HasBasis (nhds a) (fun (ε : α) => 0 < ε) fun (ε : α) => {b : α | |b - a| < ε}

theorem nhds_basis_Ioo_pos {α : Type u} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] (a : α) : Filter.HasBasis (nhds a) (fun (ε : α) => 0 < ε) fun (ε : α) => Set.Ioo (a - ε) (a + ε)

theorem nhds_basis_Icc_pos {α : Type u} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] (a : α) : Filter.HasBasis (nhds a) (fun (x : α) => 0 < x) fun (ε : α) => Set.Icc (a - ε) (a + ε)

theorem nhds_basis_zero_abs_sub_lt (α : Type u) [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] : Filter.HasBasis (nhds 0) (fun (ε : α) => 0 < ε) fun (ε : α) => {b : α | |b| < ε}

theorem nhds_basis_Ioo_pos_of_pos {α : Type u} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] {a : α} (ha : 0 < a) : Filter.HasBasis (nhds a) (fun (ε : α) => 0 < ε ∧ ε ≤ a) fun (ε : α) => Set.Ioo (a - ε) (a + ε)

If a is positive we can form a basis from only nonnegative Set.Ioo intervals

@[deprecated Set.image_neg]

theorem preimage_neg {α : Type u} [AddGroup α] : Set.preimage Neg.neg = Set.image Neg.neg

@[deprecated]

theorem Filter.map_neg_eq_comap_neg {α : Type u} [AddGroup α] : Filter.map Neg.neg = Filter.comap Neg.neg

theorem IsLUB.frequently_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : Set.Nonempty s) : ∃ᶠ (x : α) in nhdsWithin a (Set.Iic a), x ∈ s

theorem IsLUB.frequently_nhds_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : Set.Nonempty s) : ∃ᶠ (x : α) in nhds a, x ∈ s

theorem IsGLB.frequently_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsGLB s a) (hs : Set.Nonempty s) : ∃ᶠ (x : α) in nhdsWithin a (Set.Ici a), x ∈ s

theorem IsGLB.frequently_nhds_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsGLB s a) (hs : Set.Nonempty s) : ∃ᶠ (x : α) in nhds a, x ∈ s

theorem IsLUB.mem_closure {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : Set.Nonempty s) : a ∈ closure s

theorem IsGLB.mem_closure {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsGLB s a) (hs : Set.Nonempty s) : a ∈ closure s

theorem IsLUB.nhdsWithin_neBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : Set.Nonempty s) : Filter.NeBot (nhdsWithin a s)

theorem IsGLB.nhdsWithin_neBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} : IsGLB s a → Set.Nonempty s → Filter.NeBot (nhdsWithin a s)

theorem isLUB_of_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {s : Set α} {a : α} {f : Filter α} (hsa : a ∈ upperBounds s) (hsf : s ∈ f) [Filter.NeBot (f ⊓ nhds a)] : IsLUB s a

theorem isLUB_of_mem_closure {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {s : Set α} {a : α} (hsa : a ∈ upperBounds s) (hsf : a ∈ closure s) : IsLUB s a

theorem isGLB_of_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {s : Set α} {a : α} {f : Filter α} : a ∈ lowerBounds s → s ∈ f → Filter.NeBot (f ⊓ nhds a) → IsGLB s a

theorem isGLB_of_mem_closure {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {s : Set α} {a : α} (hsa : a ∈ lowerBounds s) (hsf : a ∈ closure s) : IsGLB s a

theorem IsLUB.mem_upperBounds_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : b ∈ upperBounds (f '' s)

theorem IsLUB.isLUB_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a) (hs : Set.Nonempty s) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : IsLUB (f '' s) b

theorem IsGLB.mem_lowerBounds_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsGLB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : b ∈ lowerBounds (f '' s)

theorem IsGLB.isGLB_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) : IsGLB s a → Set.Nonempty s → Filter.Tendsto f (nhdsWithin a s) (nhds b) → IsGLB (f '' s) b

theorem IsLUB.mem_lowerBounds_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s) (ha : IsLUB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : b ∈ lowerBounds (f '' s)

theorem IsLUB.isGLB_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} : AntitoneOn f s → IsLUB s a → Set.Nonempty s → Filter.Tendsto f (nhdsWithin a s) (nhds b) → IsGLB (f '' s) b

theorem IsGLB.mem_upperBounds_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s) (ha : IsGLB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : b ∈ upperBounds (f '' s)

theorem IsGLB.isLUB_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} : AntitoneOn f s → IsGLB s a → Set.Nonempty s → Filter.Tendsto f (nhdsWithin a s) (nhds b) → IsLUB (f '' s) b

theorem IsLUB.mem_of_isClosed {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : Set.Nonempty s) (sc : IsClosed s) : a ∈ s

theorem IsClosed.isLUB_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : Set.Nonempty s) (sc : IsClosed s) : a ∈ s

Alias of IsLUB.mem_of_isClosed.

theorem IsGLB.mem_of_isClosed {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsGLB s a) (hs : Set.Nonempty s) (sc : IsClosed s) : a ∈ s

theorem IsClosed.isGLB_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsGLB s a) (hs : Set.Nonempty s) (sc : IsClosed s) : a ∈ s

Alias of IsGLB.mem_of_isClosed.

Existence of sequences tending to sInf or sSup of a given set

theorem IsLUB.exists_seq_strictMono_tendsto_of_not_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α} {x : α} [Filter.IsCountablyGenerated (nhds x)] (htx : IsLUB t x) (not_mem : x ∉ t) (ht : Set.Nonempty t) : ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ ∀ (n : ℕ), u n ∈ t

theorem IsLUB.exists_seq_monotone_tendsto {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α} {x : α} [Filter.IsCountablyGenerated (nhds x)] (htx : IsLUB t x) (ht : Set.Nonempty t) : ∃ (u : ℕ → α), Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ ∀ (n : ℕ), u n ∈ t

theorem exists_seq_strictMono_tendsto' {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [DenselyOrdered α] [OrderTopology α] [FirstCountableTopology α] {x : α} {y : α} (hy : y < x) : ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo y x) ∧ Filter.Tendsto u Filter.atTop (nhds x)

theorem exists_seq_strictMono_tendsto {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α] (x : α) : ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (nhds x)

theorem exists_seq_strictMono_tendsto_nhdsWithin {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α] (x : α) : ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (nhdsWithin x (Set.Iio x))

theorem exists_seq_tendsto_sSup {α : Type u_1} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {S : Set α} (hS : Set.Nonempty S) (hS' : BddAbove S) : ∃ (u : ℕ → α), Monotone u ∧ Filter.Tendsto u Filter.atTop (nhds (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S

theorem IsGLB.exists_seq_strictAnti_tendsto_of_not_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α} {x : α} [Filter.IsCountablyGenerated (nhds x)] (htx : IsGLB t x) (not_mem : x ∉ t) (ht : Set.Nonempty t) : ∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ ∀ (n : ℕ), u n ∈ t

theorem IsGLB.exists_seq_antitone_tendsto {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α} {x : α} [Filter.IsCountablyGenerated (nhds x)] (htx : IsGLB t x) (ht : Set.Nonempty t) : ∃ (u : ℕ → α), Antitone u ∧ (∀ (n : ℕ), x ≤ u n) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ ∀ (n : ℕ), u n ∈ t

theorem exists_seq_strictAnti_tendsto' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [FirstCountableTopology α] {x : α} {y : α} (hy : x < y) : ∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo x y) ∧ Filter.Tendsto u Filter.atTop (nhds x)

theorem exists_seq_strictAnti_tendsto {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] [FirstCountableTopology α] (x : α) : ∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Filter.Tendsto u Filter.atTop (nhds x)

theorem exists_seq_strictAnti_tendsto_nhdsWithin {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] [FirstCountableTopology α] (x : α) : ∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Filter.Tendsto u Filter.atTop (nhdsWithin x (Set.Ioi x))

theorem exists_seq_strictAnti_strictMono_tendsto {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [FirstCountableTopology α] {x : α} {y : α} (h : x < y) : ∃ (u : ℕ → α) (v : ℕ → α), StrictAnti u ∧ StrictMono v ∧ (∀ (k : ℕ), u k ∈ Set.Ioo x y) ∧ (∀ (l : ℕ), v l ∈ Set.Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ Filter.Tendsto v Filter.atTop (nhds y)

theorem exists_seq_tendsto_sInf {α : Type u_1} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {S : Set α} (hS : Set.Nonempty S) (hS' : BddBelow S) : ∃ (u : ℕ → α), Antitone u ∧ Filter.Tendsto u Filter.atTop (nhds (sInf S)) ∧ ∀ (n : ℕ), u n ∈ S

theorem closure_Ioi' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (h : Set.Nonempty (Set.Ioi a)) : closure (Set.Ioi a) = Set.Ici a

The closure of the interval (a, +∞) is the closed interval [a, +∞), unless a is a top element.

@[simp]

theorem closure_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) [NoMaxOrder α] : closure (Set.Ioi a) = Set.Ici a

The closure of the interval (a, +∞) is the closed interval [a, +∞).

theorem closure_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (h : Set.Nonempty (Set.Iio a)) : closure (Set.Iio a) = Set.Iic a

The closure of the interval (-∞, a) is the closed interval (-∞, a], unless a is a bottom element.

@[simp]

theorem closure_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) [NoMinOrder α] : closure (Set.Iio a) = Set.Iic a

The closure of the interval (-∞, a) is the interval (-∞, a].

@[simp]

theorem closure_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (hab : a ≠ b) : closure (Set.Ioo a b) = Set.Icc a b

The closure of the open interval (a, b) is the closed interval [a, b].

@[simp]

theorem closure_Ioc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (hab : a ≠ b) : closure (Set.Ioc a b) = Set.Icc a b

The closure of the interval (a, b] is the closed interval [a, b].

@[simp]

theorem closure_Ico {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (hab : a ≠ b) : closure (Set.Ico a b) = Set.Icc a b

The closure of the interval [a, b) is the closed interval [a, b].

@[simp]

theorem interior_Ici' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : Set.Nonempty (Set.Iio a)) : interior (Set.Ici a) = Set.Ioi a

theorem interior_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} : interior (Set.Ici a) = Set.Ioi a

@[simp]

theorem interior_Iic' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : Set.Nonempty (Set.Ioi a)) : interior (Set.Iic a) = Set.Iio a

theorem interior_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} : interior (Set.Iic a) = Set.Iio a

@[simp]

theorem interior_Icc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] {a : α} {b : α} : interior (Set.Icc a b) = Set.Ioo a b

@[simp]

theorem Icc_mem_nhds_iff {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] {a : α} {b : α} {x : α} : Set.Icc a b ∈ nhds x ↔ x ∈ Set.Ioo a b

@[simp]

theorem interior_Ico {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} {b : α} : interior (Set.Ico a b) = Set.Ioo a b

@[simp]

theorem Ico_mem_nhds_iff {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} {b : α} {x : α} : Set.Ico a b ∈ nhds x ↔ x ∈ Set.Ioo a b

@[simp]

theorem interior_Ioc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} {b : α} : interior (Set.Ioc a b) = Set.Ioo a b

@[simp]

theorem Ioc_mem_nhds_iff {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} {b : α} {x : α} : Set.Ioc a b ∈ nhds x ↔ x ∈ Set.Ioo a b

theorem closure_interior_Icc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (h : a ≠ b) : closure (interior (Set.Icc a b)) = Set.Icc a b

theorem Ioc_subset_closure_interior {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) (b : α) : Set.Ioc a b ⊆ closure (interior (Set.Ioc a b))

theorem Ico_subset_closure_interior {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) (b : α) : Set.Ico a b ⊆ closure (interior (Set.Ico a b))

@[simp]

theorem frontier_Ici' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : Set.Nonempty (Set.Iio a)) : frontier (Set.Ici a) = {a}

theorem frontier_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} : frontier (Set.Ici a) = {a}

@[simp]

theorem frontier_Iic' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : Set.Nonempty (Set.Ioi a)) : frontier (Set.Iic a) = {a}

theorem frontier_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} : frontier (Set.Iic a) = {a}

@[simp]

theorem frontier_Ioi' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : Set.Nonempty (Set.Ioi a)) : frontier (Set.Ioi a) = {a}

theorem frontier_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} : frontier (Set.Ioi a) = {a}

@[simp]

theorem frontier_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : Set.Nonempty (Set.Iio a)) : frontier (Set.Iio a) = {a}

theorem frontier_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} : frontier (Set.Iio a) = {a}

@[simp]

theorem frontier_Icc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] {a : α} {b : α} (h : a ≤ b) : frontier (Set.Icc a b) = {a, b}

@[simp]

theorem frontier_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (h : a < b) : frontier (Set.Ioo a b) = {a, b}

@[simp]

theorem frontier_Ico {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} {b : α} (h : a < b) : frontier (Set.Ico a b) = {a, b}

@[simp]

theorem frontier_Ioc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} {b : α} (h : a < b) : frontier (Set.Ioc a b) = {a, b}

theorem nhdsWithin_Ioi_neBot' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (H₁ : Set.Nonempty (Set.Ioi a)) (H₂ : a ≤ b) : Filter.NeBot (nhdsWithin b (Set.Ioi a))

theorem nhdsWithin_Ioi_neBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} {b : α} (H : a ≤ b) : Filter.NeBot (nhdsWithin b (Set.Ioi a))

theorem nhdsWithin_Ioi_self_neBot' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (H : Set.Nonempty (Set.Ioi a)) : Filter.NeBot (nhdsWithin a (Set.Ioi a))

instance nhdsWithin_Ioi_self_neBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] (a : α) : Filter.NeBot (nhdsWithin a (Set.Ioi a))

Equations

• ⋯ = ⋯

theorem nhdsWithin_Iio_neBot' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {b : α} {c : α} (H₁ : Set.Nonempty (Set.Iio c)) (H₂ : b ≤ c) : Filter.NeBot (nhdsWithin b (Set.Iio c))

theorem nhdsWithin_Iio_neBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} {b : α} (H : a ≤ b) : Filter.NeBot (nhdsWithin a (Set.Iio b))

theorem nhdsWithin_Iio_self_neBot' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {b : α} (H : Set.Nonempty (Set.Iio b)) : Filter.NeBot (nhdsWithin b (Set.Iio b))

instance nhdsWithin_Iio_self_neBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] (a : α) : Filter.NeBot (nhdsWithin a (Set.Iio a))

Equations

• ⋯ = ⋯

theorem right_nhdsWithin_Ico_neBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (H : a < b) : Filter.NeBot (nhdsWithin b (Set.Ico a b))

theorem left_nhdsWithin_Ioc_neBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (H : a < b) : Filter.NeBot (nhdsWithin a (Set.Ioc a b))

theorem left_nhdsWithin_Ioo_neBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (H : a < b) : Filter.NeBot (nhdsWithin a (Set.Ioo a b))

theorem right_nhdsWithin_Ioo_neBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (H : a < b) : Filter.NeBot (nhdsWithin b (Set.Ioo a b))

theorem comap_coe_nhdsWithin_Iio_of_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {b : α} {s : Set α} (hb : s ⊆ Set.Iio b) (hs : Set.Nonempty s → ∃ a < b, Set.Ioo a b ⊆ s) : Filter.comap Subtype.val (nhdsWithin b (Set.Iio b)) = Filter.atTop

theorem comap_coe_nhdsWithin_Ioi_of_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {s : Set α} (ha : s ⊆ Set.Ioi a) (hs : Set.Nonempty s → ∃ b > a, Set.Ioo a b ⊆ s) : Filter.comap Subtype.val (nhdsWithin a (Set.Ioi a)) = Filter.atBot

theorem map_coe_atTop_of_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {b : α} {s : Set α} (hb : s ⊆ Set.Iio b) (hs : ∀ a' < b, ∃ a < b, Set.Ioo a b ⊆ s) : Filter.map Subtype.val Filter.atTop = nhdsWithin b (Set.Iio b)

theorem map_coe_atBot_of_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {s : Set α} (ha : s ⊆ Set.Ioi a) (hs : ∀ b' > a, ∃ b > a, Set.Ioo a b ⊆ s) : Filter.map Subtype.val Filter.atBot = nhdsWithin a (Set.Ioi a)

theorem comap_coe_Ioo_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) (b : α) : Filter.comap Subtype.val (nhdsWithin b (Set.Iio b)) = Filter.atTop

The atTop filter for an open interval Ioo a b comes from the left-neighbourhoods filter at the right endpoint in the ambient order.

theorem comap_coe_Ioo_nhdsWithin_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) (b : α) : Filter.comap Subtype.val (nhdsWithin a (Set.Ioi a)) = Filter.atBot

The atBot filter for an open interval Ioo a b comes from the right-neighbourhoods filter at the left endpoint in the ambient order.

theorem comap_coe_Ioi_nhdsWithin_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) : Filter.comap Subtype.val (nhdsWithin a (Set.Ioi a)) = Filter.atBot

theorem comap_coe_Iio_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) : Filter.comap Subtype.val (nhdsWithin a (Set.Iio a)) = Filter.atTop

@[simp]

theorem map_coe_Ioo_atTop {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (h : a < b) : Filter.map Subtype.val Filter.atTop = nhdsWithin b (Set.Iio b)

@[simp]

theorem map_coe_Ioo_atBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (h : a < b) : Filter.map Subtype.val Filter.atBot = nhdsWithin a (Set.Ioi a)

@[simp]

theorem map_coe_Ioi_atBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) : Filter.map Subtype.val Filter.atBot = nhdsWithin a (Set.Ioi a)

@[simp]

theorem map_coe_Iio_atTop {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) : Filter.map Subtype.val Filter.atTop = nhdsWithin a (Set.Iio a)

@[simp]

theorem tendsto_comp_coe_Ioo_atTop {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} {l : Filter β} {f : α → β} (h : a < b) : Filter.Tendsto (fun (x : ↑(Set.Ioo a b)) => f ↑x) Filter.atTop l ↔ Filter.Tendsto f (nhdsWithin b (Set.Iio b)) l

@[simp]

theorem tendsto_comp_coe_Ioo_atBot {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} {l : Filter β} {f : α → β} (h : a < b) : Filter.Tendsto (fun (x : ↑(Set.Ioo a b)) => f ↑x) Filter.atBot l ↔ Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) l

@[simp]

theorem tendsto_comp_coe_Ioi_atBot {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {l : Filter β} {f : α → β} : Filter.Tendsto (fun (x : ↑(Set.Ioi a)) => f ↑x) Filter.atBot l ↔ Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) l

@[simp]

theorem tendsto_comp_coe_Iio_atTop {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {l : Filter β} {f : α → β} : Filter.Tendsto (fun (x : ↑(Set.Iio a)) => f ↑x) Filter.atTop l ↔ Filter.Tendsto f (nhdsWithin a (Set.Iio a)) l

@[simp]

theorem tendsto_Ioo_atTop {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} {l : Filter β} {f : β → ↑(Set.Ioo a b)} : Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l (nhdsWithin b (Set.Iio b))

@[simp]

theorem tendsto_Ioo_atBot {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} {l : Filter β} {f : β → ↑(Set.Ioo a b)} : Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l (nhdsWithin a (Set.Ioi a))

@[simp]

theorem tendsto_Ioi_atBot {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {l : Filter β} {f : β → ↑(Set.Ioi a)} : Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l (nhdsWithin a (Set.Ioi a))

@[simp]

theorem tendsto_Iio_atTop {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {l : Filter β} {f : β → ↑(Set.Iio a)} : Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l (nhdsWithin a (Set.Iio a))

instance instNeBotNhdsWithinComplSetInstHasComplSetSingletonInstSingletonSet {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (x : α) [Nontrivial α] : Filter.NeBot (nhdsWithin x {x}ᶜ)

Equations

• ⋯ = ⋯

theorem Dense.exists_countable_dense_subset_no_bot_top {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [Nontrivial α] {s : Set α} [TopologicalSpace.SeparableSpace ↑s] (hs : Dense s) : ∃ t ⊆ s, Set.Countable t ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t

Let s be a dense set in a nontrivial dense linear order α. If s is a separable space (e.g., if α has a second countable topology), then there exists a countable dense subset t ⊆ s such that t does not contain bottom/top elements of α.

theorem exists_countable_dense_no_bot_top (α : Type u) [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [TopologicalSpace.SeparableSpace α] [Nontrivial α] : ∃ (s : Set α), Set.Countable s ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∉ s) ∧ ∀ (x : α), IsTop x → x ∉ s

If α is a nontrivial separable dense linear order, then there exists a countable dense set s : Set α that contains neither top nor bottom elements of α. For a dense set containing both bot and top elements, see exists_countable_dense_bot_top.

theorem Monotone.map_sSup_of_continuousAt' {α : Type u} {β : Type v} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousAt f (sSup A)) (Mf : Monotone f) (A_nonemp : Set.Nonempty A) (A_bdd : autoParam (BddAbove A) _auto✝) : f (sSup A) = sSup (f '' A)

A monotone function continuous at the supremum of a nonempty set sends this supremum to the supremum of the image of this set.

theorem Monotone.map_iSup_of_continuousAt' {α : Type u} {β : Type v} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_1} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Mf : Monotone f) (bdd : autoParam (BddAbove (Set.range g)) _auto✝) : f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

A monotone function continuous at the indexed supremum over a nonempty Sort sends this indexed supremum to the indexed supremum of the composition.

theorem Monotone.map_sInf_of_continuousAt' {α : Type u} {β : Type v} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousAt f (sInf A)) (Mf : Monotone f) (A_nonemp : Set.Nonempty A) (A_bdd : autoParam (BddBelow A) _auto✝) : f (sInf A) = sInf (f '' A)

A monotone function continuous at the infimum of a nonempty set sends this infimum to the infimum of the image of this set.

theorem Monotone.map_iInf_of_continuousAt' {α : Type u} {β : Type v} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_1} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Mf : Monotone f) (bdd : autoParam (BddBelow (Set.range g)) _auto✝) : f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)

A monotone function continuous at the indexed infimum over a nonempty Sort sends this indexed infimum to the indexed infimum of the composition.

theorem Antitone.map_sInf_of_continuousAt' {α : Type u} {β : Type v} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousAt f (sInf A)) (Af : Antitone f) (A_nonemp : Set.Nonempty A) (A_bdd : autoParam (BddBelow A) _auto✝) : f (sInf A) = sSup (f '' A)

An antitone function continuous at the infimum of a nonempty set sends this infimum to the supremum of the image of this set.

theorem Antitone.map_iInf_of_continuousAt' {α : Type u} {β : Type v} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_1} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Af : Antitone f) (bdd : autoParam (BddBelow (Set.range g)) _auto✝) : f (⨅ (i : ι), g i) = ⨆ (i : ι), f (g i)

An antitone function continuous at the indexed infimum over a nonempty Sort sends this indexed infimum to the indexed supremum of the composition.

theorem Antitone.map_sSup_of_continuousAt' {α : Type u} {β : Type v} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousAt f (sSup A)) (Af : Antitone f) (A_nonemp : Set.Nonempty A) (A_bdd : autoParam (BddAbove A) _auto✝) : f (sSup A) = sInf (f '' A)

An antitone function continuous at the supremum of a nonempty set sends this supremum to the infimum of the image of this set.

theorem Antitone.map_iSup_of_continuousAt' {α : Type u} {β : Type v} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_1} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Af : Antitone f) (bdd : autoParam (BddAbove (Set.range g)) _auto✝) : f (⨆ (i : ι), g i) = ⨅ (i : ι), f (g i)

An antitone function continuous at the indexed supremum over a nonempty Sort sends this indexed supremum to the indexed infimum of the composition.

theorem sSup_mem_closure {α : Type u} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α] {s : Set α} (hs : Set.Nonempty s) : sSup s ∈ closure s

theorem sInf_mem_closure {α : Type u} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α] {s : Set α} (hs : Set.Nonempty s) : sInf s ∈ closure s

theorem IsClosed.sSup_mem {α : Type u} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α] {s : Set α} (hs : Set.Nonempty s) (hc : IsClosed s) : sSup s ∈ s

theorem IsClosed.sInf_mem {α : Type u} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α] {s : Set α} (hs : Set.Nonempty s) (hc : IsClosed s) : sInf s ∈ s

theorem Monotone.map_sSup_of_continuousAt {α : Type u} {β : Type v} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Mf : Monotone f) (fbot : f ⊥ = ⊥) : f (sSup s) = sSup (f '' s)

A monotone function f sending bot to bot and continuous at the supremum of a set sends this supremum to the supremum of the image of this set.

theorem Monotone.map_iSup_of_continuousAt {α : Type u} {β : Type v} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_1} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Mf : Monotone f) (fbot : f ⊥ = ⊥) : f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

If a monotone function sending bot to bot is continuous at the indexed supremum over a Sort, then it sends this indexed supremum to the indexed supremum of the composition.

theorem Monotone.map_sInf_of_continuousAt {α : Type u} {β : Type v} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Mf : Monotone f) (ftop : f ⊤ = ⊤) : f (sInf s) = sInf (f '' s)

A monotone function f sending top to top and continuous at the infimum of a set sends this infimum to the infimum of the image of this set.

theorem Monotone.map_iInf_of_continuousAt {α : Type u} {β : Type v} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_1} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Mf : Monotone f) (ftop : f ⊤ = ⊤) : f (iInf g) = iInf (f ∘ g)

If a monotone function sending top to top is continuous at the indexed infimum over a Sort, then it sends this indexed infimum to the indexed infimum of the composition.

theorem Antitone.map_sSup_of_continuousAt {α : Type u} {β : Type v} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Af : Antitone f) (fbot : f ⊥ = ⊤) : f (sSup s) = sInf (f '' s)

An antitone function f sending bot to top and continuous at the supremum of a set sends this supremum to the infimum of the image of this set.

theorem Antitone.map_iSup_of_continuousAt {α : Type u} {β : Type v} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_1} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Af : Antitone f) (fbot : f ⊥ = ⊤) : f (⨆ (i : ι), g i) = ⨅ (i : ι), f (g i)

An antitone function sending bot to top is continuous at the indexed supremum over a Sort, then it sends this indexed supremum to the indexed supremum of the composition.

theorem Antitone.map_sInf_of_continuousAt {α : Type u} {β : Type v} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Af : Antitone f) (ftop : f ⊤ = ⊥) : f (sInf s) = sSup (f '' s)

An antitone function f sending top to bot and continuous at the infimum of a set sends this infimum to the supremum of the image of this set.

theorem Antitone.map_iInf_of_continuousAt {α : Type u} {β : Type v} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_1} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Af : Antitone f) (ftop : f ⊤ = ⊥) : f (iInf g) = iSup (f ∘ g)

If an antitone function sending top to bot is continuous at the indexed infimum over a Sort, then it sends this indexed infimum to the indexed supremum of the composition.

theorem csSup_mem_closure {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hs : Set.Nonempty s) (B : BddAbove s) : sSup s ∈ closure s

theorem csInf_mem_closure {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hs : Set.Nonempty s) (B : BddBelow s) : sInf s ∈ closure s

theorem IsClosed.csSup_mem {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hc : IsClosed s) (hs : Set.Nonempty s) (B : BddAbove s) : sSup s ∈ s

theorem IsClosed.csInf_mem {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hc : IsClosed s) (hs : Set.Nonempty s) (B : BddBelow s) : sInf s ∈ s

theorem IsClosed.isLeast_csInf {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hc : IsClosed s) (hs : Set.Nonempty s) (B : BddBelow s) : IsLeast s (sInf s)

theorem IsClosed.isGreatest_csSup {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hc : IsClosed s) (hs : Set.Nonempty s) (B : BddAbove s) : IsGreatest s (sSup s)

theorem Monotone.map_csSup_of_continuousAt {α : Type u} {β : Type v} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Mf : Monotone f) (ne : Set.Nonempty s) (H : BddAbove s) : f (sSup s) = sSup (f '' s)

If a monotone function is continuous at the supremum of a nonempty bounded above set s, then it sends this supremum to the supremum of the image of s.

theorem Monotone.map_ciSup_of_continuousAt {α : Type u} {β : Type v} {γ : Type w} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] [Nonempty γ] {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨆ (i : γ), g i)) (Mf : Monotone f) (H : BddAbove (Set.range g)) : f (⨆ (i : γ), g i) = ⨆ (i : γ), f (g i)

If a monotone function is continuous at the indexed supremum of a bounded function on a nonempty Sort, then it sends this supremum to the supremum of the composition.

theorem Monotone.map_csInf_of_continuousAt {α : Type u} {β : Type v} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Mf : Monotone f) (ne : Set.Nonempty s) (H : BddBelow s) : f (sInf s) = sInf (f '' s)

If a monotone function is continuous at the infimum of a nonempty bounded below set s, then it sends this infimum to the infimum of the image of s.

theorem Monotone.map_ciInf_of_continuousAt {α : Type u} {β : Type v} {γ : Type w} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] [Nonempty γ] {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨅ (i : γ), g i)) (Mf : Monotone f) (H : BddBelow (Set.range g)) : f (⨅ (i : γ), g i) = ⨅ (i : γ), f (g i)

A continuous monotone function sends indexed infimum to indexed infimum in conditionally complete linear order, under a boundedness assumption.

theorem Antitone.map_csSup_of_continuousAt {α : Type u} {β : Type v} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Af : Antitone f) (ne : Set.Nonempty s) (H : BddAbove s) : f (sSup s) = sInf (f '' s)

If an antitone function is continuous at the supremum of a nonempty bounded above set s, then it sends this supremum to the infimum of the image of s.

theorem Antitone.map_ciSup_of_continuousAt {α : Type u} {β : Type v} {γ : Type w} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] [Nonempty γ] {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨆ (i : γ), g i)) (Af : Antitone f) (H : BddAbove (Set.range g)) : f (⨆ (i : γ), g i) = ⨅ (i : γ), f (g i)

If an antitone function is continuous at the indexed supremum of a bounded function on a nonempty Sort, then it sends this supremum to the infimum of the composition.

theorem Antitone.map_csInf_of_continuousAt {α : Type u} {β : Type v} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Af : Antitone f) (ne : Set.Nonempty s) (H : BddBelow s) : f (sInf s) = sSup (f '' s)

If an antitone function is continuous at the infimum of a nonempty bounded below set s, then it sends this infimum to the supremum of the image of s.

theorem Antitone.map_ciInf_of_continuousAt {α : Type u} {β : Type v} {γ : Type w} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] [Nonempty γ] {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨅ (i : γ), g i)) (Af : Antitone f) (H : BddBelow (Set.range g)) : f (⨅ (i : γ), g i) = ⨆ (i : γ), f (g i)

A continuous antitone function sends indexed infimum to indexed supremum in conditionally complete linear order, under a boundedness assumption.

theorem Monotone.tendsto_nhdsWithin_Iio {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (Mf : Monotone f) (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sSup (f '' Set.Iio x)))

A monotone map has a limit to the left of any point x, equal to sSup (f '' (Iio x)).

theorem Monotone.tendsto_nhdsWithin_Ioi {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (Mf : Monotone f) (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sInf (f '' Set.Ioi x)))

A monotone map has a limit to the right of any point x, equal to sInf (f '' (Ioi x)).