mathlib documentation

topology.algebra.ordered

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 order_topology α(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 also introduce another (mixin) class order_closed_topology α saying that the set of points (x, y) with x ≤ y is closed in the product space. This is automatically satisfied on a linear order with 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 (order_closed_topology vs order_topology, preorder vs partial_order vs linear_order etc) see their statements.

Open / closed sets #

Convergence and inequalities #

Min, max, Sup and Inf #

Connected sets and Intermediate Value Theorem #

Miscellaneous facts #

Implementation #

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]
structure order_closed_topology (α : Type u_1) [topological_space α] [preorder α] :
Prop

A topology on a set which is both a topological space and a preorder is order-closed if the set of points (x, y) with x ≤ y is closed in the product space. We introduce this as a mixin. This property is satisfied for the order topology on a linear order, but it can be satisfied more generally, and suffices to derive many interesting properties relating order and topology.

Instances
@[protected, instance]
Equations
theorem is_closed_le_prod {α : Type u} [topological_space α] [preorder α] [t : order_closed_topology α] :
is_closed {p : α × α | p.fst p.snd}
theorem is_closed_le {α : Type u} {β : Type v} [topological_space α] [preorder α] [t : order_closed_topology α] [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
is_closed {b : β | f b g b}
theorem is_closed_le' {α : Type u} [topological_space α] [preorder α] [t : order_closed_topology α] (a : α) :
is_closed {b : α | b a}
theorem is_closed_Iic {α : Type u} [topological_space α] [preorder α] [t : order_closed_topology α] {a : α} :
theorem is_closed_ge' {α : Type u} [topological_space α] [preorder α] [t : order_closed_topology α] (a : α) :
is_closed {b : α | a b}
theorem is_closed_Ici {α : Type u} [topological_space α] [preorder α] [t : order_closed_topology α] {a : α} :
theorem is_closed_Icc {α : Type u} [topological_space α] [preorder α] [t : order_closed_topology α] {a b : α} :
@[simp]
theorem closure_Icc {α : Type u} [topological_space α] [preorder α] [t : order_closed_topology α] (a b : α) :
@[simp]
theorem closure_Iic {α : Type u} [topological_space α] [preorder α] [t : order_closed_topology α] (a : α) :
@[simp]
theorem closure_Ici {α : Type u} [topological_space α] [preorder α] [t : order_closed_topology α] (a : α) :
theorem le_of_tendsto_of_tendsto {α : Type u} {β : Type v} [topological_space α] [preorder α] [t : order_closed_topology α] {f g : β → α} {b : filter β} {a₁ a₂ : α} [b.ne_bot] (hf : filter.tendsto f b (𝓝 a₁)) (hg : filter.tendsto g b (𝓝 a₂)) (h : f ≤ᶠ[b] g) :
a₁ a₂
theorem le_of_tendsto_of_tendsto' {α : Type u} {β : Type v} [topological_space α] [preorder α] [t : order_closed_topology α] {f g : β → α} {b : filter β} {a₁ a₂ : α} [b.ne_bot] (hf : filter.tendsto f b (𝓝 a₁)) (hg : filter.tendsto g b (𝓝 a₂)) (h : ∀ (x : β), f x g x) :
a₁ a₂
theorem le_of_tendsto {α : Type u} {β : Type v} [topological_space α] [preorder α] [t : order_closed_topology α] {f : β → α} {a b : α} {x : filter β} [x.ne_bot] (lim : filter.tendsto f x (𝓝 a)) (h : ∀ᶠ (c : β) in x, f c b) :
a b
theorem le_of_tendsto' {α : Type u} {β : Type v} [topological_space α] [preorder α] [t : order_closed_topology α] {f : β → α} {a b : α} {x : filter β} [x.ne_bot] (lim : filter.tendsto f x (𝓝 a)) (h : ∀ (c : β), f c b) :
a b
theorem ge_of_tendsto {α : Type u} {β : Type v} [topological_space α] [preorder α] [t : order_closed_topology α] {f : β → α} {a b : α} {x : filter β} [x.ne_bot] (lim : filter.tendsto f x (𝓝 a)) (h : ∀ᶠ (c : β) in x, b f c) :
b a
theorem ge_of_tendsto' {α : Type u} {β : Type v} [topological_space α] [preorder α] [t : order_closed_topology α] {f : β → α} {a b : α} {x : filter β} [x.ne_bot] (lim : filter.tendsto f x (𝓝 a)) (h : ∀ (c : β), b f c) :
b a
@[simp]
theorem closure_le_eq {α : Type u} {β : Type v} [topological_space α] [preorder α] [t : order_closed_topology α] [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
closure {b : β | f b g b} = {b : β | f b g b}
theorem closure_lt_subset_le {α : Type u} {β : Type v} [topological_space α] [preorder α] [t : order_closed_topology α] [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
closure {b : β | f b < g b} {b : β | f b g b}
theorem continuous_within_at.closure_le {α : Type u} {β : Type v} [topological_space α] [preorder α] [t : order_closed_topology α] [topological_space β] {f g : β → α} {s : set β} {x : β} (hx : x closure s) (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) (h : ∀ (y : β), y sf y g y) :
f x g x
theorem is_closed.is_closed_le {α : Type u} {β : Type v} [topological_space α] [preorder α] [t : order_closed_topology α] [topological_space β] {f g : β → α} {s : set β} (hs : is_closed s) (hf : continuous_on f s) (hg : continuous_on g s) :
is_closed {x ∈ s | f x g x}

If s is a closed set and two functions f and g are continuous on s, then the set {x ∈ s | f x ≤ g x} is a closed set.

theorem nhds_within_Ici_ne_bot {α : Type u} [topological_space α] [preorder α] {a b : α} (H₂ : a b) :
@[instance]
theorem nhds_within_Ici_self_ne_bot {α : Type u} [topological_space α] [preorder α] (a : α) :
theorem nhds_within_Iic_ne_bot {α : Type u} [topological_space α] [preorder α] {a b : α} (H : a b) :
@[instance]
theorem nhds_within_Iic_self_ne_bot {α : Type u} [topological_space α] [preorder α] (a : α) :
@[protected, instance]
theorem is_open_lt_prod {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] :
is_open {p : α × α | p.fst < p.snd}
theorem is_open_lt {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
is_open {b : β | f b < g b}
theorem is_open_Iio {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a : α} :
theorem is_open_Ioi {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a : α} :
theorem is_open_Ioo {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b : α} :
@[simp]
theorem interior_Ioi {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a : α} :
@[simp]
theorem interior_Iio {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a : α} :
@[simp]
theorem interior_Ioo {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b : α} :
theorem eventually_le_of_tendsto_lt {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] {l : filter γ} {f : γ → α} {u v : α} (hv : v < u) (h : filter.tendsto f l (𝓝 v)) :
∀ᶠ (a : γ) in l, f a u
theorem eventually_ge_of_tendsto_gt {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] {l : filter γ} {f : γ → α} {u v : α} (hv : u < v) (h : filter.tendsto f l (𝓝 v)) :
∀ᶠ (a : γ) in l, u f a
theorem intermediate_value_univ₂ {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] [preconnected_space γ] {a b : γ} {f g : γ → α} (hf : continuous f) (hg : continuous g) (ha : f a g a) (hb : g b f b) :
∃ (x : γ), f x = g x

Intermediate value theorem for two functions: if f and g are two continuous functions on a preconnected space and f a ≤ g a and g b ≤ f b, then for some x we have f x = g x.

theorem intermediate_value_univ₂_eventually₁ {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] [preconnected_space γ] {a : γ} {l : filter γ} [l.ne_bot] {f g : γ → α} (hf : continuous f) (hg : continuous g) (ha : f a g a) (he : g ≤ᶠ[l] f) :
∃ (x : γ), f x = g x
theorem intermediate_value_univ₂_eventually₂ {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] [preconnected_space γ] {l₁ l₂ : filter γ} [l₁.ne_bot] [l₂.ne_bot] {f g : γ → α} (hf : continuous f) (hg : continuous g) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) :
∃ (x : γ), f x = g x
theorem is_preconnected.intermediate_value₂ {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] {s : set γ} (hs : is_preconnected s) {a b : γ} (ha : a s) (hb : b s) {f g : γ → α} (hf : continuous_on f s) (hg : continuous_on g s) (ha' : f a g a) (hb' : g b f b) :
∃ (x : γ) (H : x s), f x = g x

Intermediate value theorem for two functions: if f and g are two functions continuous on a preconnected set s and for some a b ∈ s we have f a ≤ g a and g b ≤ f b, then for some x ∈ s we have f x = g x.

theorem is_preconnected.intermediate_value₂_eventually₁ {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] {s : set γ} (hs : is_preconnected s) {a : γ} {l : filter γ} (ha : a s) [l.ne_bot] (hl : l 𝓟 s) {f g : γ → α} (hf : continuous_on f s) (hg : continuous_on g s) (ha' : f a g a) (he : g ≤ᶠ[l] f) :
∃ (x : γ) (H : x s), f x = g x
theorem is_preconnected.intermediate_value₂_eventually₂ {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] {s : set γ} (hs : is_preconnected s) {l₁ l₂ : filter γ} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ 𝓟 s) (hl₂ : l₂ 𝓟 s) {f g : γ → α} (hf : continuous_on f s) (hg : continuous_on g s) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) :
∃ (x : γ) (H : x s), f x = g x
theorem is_preconnected.intermediate_value {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] {s : set γ} (hs : is_preconnected s) {a b : γ} (ha : a s) (hb : b s) {f : γ → α} (hf : continuous_on f s) :
set.Icc (f a) (f b) f '' s

Intermediate Value Theorem for continuous functions on connected sets.

theorem is_preconnected.intermediate_value_Ico {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] {s : set γ} (hs : is_preconnected s) {a : γ} {l : filter γ} (ha : a s) [l.ne_bot] (hl : l 𝓟 s) {f : γ → α} (hf : continuous_on f s) {v : α} (ht : filter.tendsto f l (𝓝 v)) :
set.Ico (f a) v f '' s
theorem is_preconnected.intermediate_value_Ioc {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] {s : set γ} (hs : is_preconnected s) {a : γ} {l : filter γ} (ha : a s) [l.ne_bot] (hl : l 𝓟 s) {f : γ → α} (hf : continuous_on f s) {v : α} (ht : filter.tendsto f l (𝓝 v)) :
set.Ioc v (f a) f '' s
theorem is_preconnected.intermediate_value_Ioo {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] {s : set γ} (hs : is_preconnected s) {l₁ l₂ : filter γ} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ 𝓟 s) (hl₂ : l₂ 𝓟 s) {f : γ → α} (hf : continuous_on f s) {v₁ v₂ : α} (ht₁ : filter.tendsto f l₁ (𝓝 v₁)) (ht₂ : filter.tendsto f l₂ (𝓝 v₂)) :
set.Ioo v₁ v₂ f '' s
theorem is_preconnected.intermediate_value_Ici {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] {s : set γ} (hs : is_preconnected s) {a : γ} {l : filter γ} (ha : a s) [l.ne_bot] (hl : l 𝓟 s) {f : γ → α} (hf : continuous_on f s) (ht : filter.tendsto f l filter.at_top) :
set.Ici (f a) f '' s
theorem is_preconnected.intermediate_value_Iic {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] {s : set γ} (hs : is_preconnected s) {a : γ} {l : filter γ} (ha : a s) [l.ne_bot] (hl : l 𝓟 s) {f : γ → α} (hf : continuous_on f s) (ht : filter.tendsto f l filter.at_bot) :
set.Iic (f a) f '' s
theorem is_preconnected.intermediate_value_Ioi {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] {s : set γ} (hs : is_preconnected s) {l₁ l₂ : filter γ} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ 𝓟 s) (hl₂ : l₂ 𝓟 s) {f : γ → α} (hf : continuous_on f s) {v : α} (ht₁ : filter.tendsto f l₁ (𝓝 v)) (ht₂ : filter.tendsto f l₂ filter.at_top) :
set.Ioi v f '' s
theorem is_preconnected.intermediate_value_Iio {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] {s : set γ} (hs : is_preconnected s) {l₁ l₂ : filter γ} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ 𝓟 s) (hl₂ : l₂ 𝓟 s) {f : γ → α} (hf : continuous_on f s) {v : α} (ht₁ : filter.tendsto f l₁ filter.at_bot) (ht₂ : filter.tendsto f l₂ (𝓝 v)) :
set.Iio v f '' s
theorem is_preconnected.intermediate_value_Iii {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] {s : set γ} (hs : is_preconnected s) {l₁ l₂ : filter γ} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ 𝓟 s) (hl₂ : l₂ 𝓟 s) {f : γ → α} (hf : continuous_on f s) (ht₁ : filter.tendsto f l₁ filter.at_bot) (ht₂ : filter.tendsto f l₂ filter.at_top) :
theorem intermediate_value_univ {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] [preconnected_space γ] (a b : γ) {f : γ → α} (hf : continuous f) :
set.Icc (f a) (f b) set.range f

Intermediate Value Theorem for continuous functions on connected spaces.

theorem mem_range_of_exists_le_of_exists_ge {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] [preconnected_space γ] {c : α} {f : γ → α} (hf : continuous f) (h₁ : ∃ (a : γ), f a c) (h₂ : ∃ (b : γ), c f b) :

Intermediate Value Theorem for continuous functions on connected spaces.

theorem is_preconnected.Icc_subset {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {s : set α} (hs : is_preconnected s) {a b : α} (ha : a s) (hb : b s) :
set.Icc a b s

If a preconnected set contains endpoints of an interval, then it includes the whole interval.

theorem is_connected.Icc_subset {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {s : set α} (hs : is_connected s) {a b : α} (ha : a s) (hb : b s) :
set.Icc a b s

If a preconnected set contains endpoints of an interval, then it includes the whole interval.

If preconnected set in a linear order space is unbounded below and above, then it is the whole space.

Neighborhoods to the left and to the right on an order_closed_topology #

Limits to the left and to the right of real functions are defined in terms of neighborhoods to the left and to the right, either open or closed, i.e., members of 𝓝[Ioi a] a and 𝓝[Ici a] a on the right, and similarly on the left. Here we simply prove that all right-neighborhoods of a point are equal, and we'll prove later other useful characterizations which require the stronger hypothesis order_topology α

Right neighborhoods, point excluded #

theorem Ioo_mem_nhds_within_Ioi {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ico a c) :
theorem Ioc_mem_nhds_within_Ioi {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ico a c) :
theorem Ico_mem_nhds_within_Ioi {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ico a c) :
theorem Icc_mem_nhds_within_Ioi {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ico a c) :
@[simp]
theorem nhds_within_Ioc_eq_nhds_within_Ioi {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b : α} (h : a < b) :
@[simp]
theorem nhds_within_Ioo_eq_nhds_within_Ioi {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b : α} (h : a < b) :
@[simp]
theorem continuous_within_at_Ioc_iff_Ioi {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space β] {a b : α} {f : α → β} (h : a < b) :
@[simp]
theorem continuous_within_at_Ioo_iff_Ioi {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space β] {a b : α} {f : α → β} (h : a < b) :

Left neighborhoods, point excluded #

theorem Ioo_mem_nhds_within_Iio {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ioc a c) :
theorem Ico_mem_nhds_within_Iio {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ioc a c) :
theorem Ioc_mem_nhds_within_Iio {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ioc a c) :
theorem Icc_mem_nhds_within_Iio {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ioc a c) :
@[simp]
theorem nhds_within_Ico_eq_nhds_within_Iio {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b : α} (h : a < b) :
@[simp]
theorem nhds_within_Ioo_eq_nhds_within_Iio {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b : α} (h : a < b) :
@[simp]
theorem continuous_within_at_Ico_iff_Iio {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] {a b : α} {f : α → γ} (h : a < b) :
@[simp]
theorem continuous_within_at_Ioo_iff_Iio {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space γ] {a b : α} {f : α → γ} (h : a < b) :

Right neighborhoods, point included #

theorem Ioo_mem_nhds_within_Ici {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ioo a c) :
theorem Ioc_mem_nhds_within_Ici {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ioo a c) :
theorem Ico_mem_nhds_within_Ici {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ico a c) :
theorem Icc_mem_nhds_within_Ici {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ico a c) :
@[simp]
theorem nhds_within_Icc_eq_nhds_within_Ici {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b : α} (h : a < b) :
@[simp]
theorem nhds_within_Ico_eq_nhds_within_Ici {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b : α} (h : a < b) :
@[simp]
theorem continuous_within_at_Icc_iff_Ici {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space β] {a b : α} {f : α → β} (h : a < b) :
@[simp]
theorem continuous_within_at_Ico_iff_Ici {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space β] {a b : α} {f : α → β} (h : a < b) :

Left neighborhoods, point included #

theorem Ioo_mem_nhds_within_Iic {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ioo a c) :
theorem Ico_mem_nhds_within_Iic {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ioo a c) :
theorem Ioc_mem_nhds_within_Iic {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ioc a c) :
theorem Icc_mem_nhds_within_Iic {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b c : α} (H : b set.Ioc a c) :
@[simp]
theorem nhds_within_Icc_eq_nhds_within_Iic {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b : α} (h : a < b) :
@[simp]
theorem nhds_within_Ioc_eq_nhds_within_Iic {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] {a b : α} (h : a < b) :
@[simp]
theorem continuous_within_at_Icc_iff_Iic {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space β] {a b : α} {f : α → β} (h : a < b) :
@[simp]
theorem continuous_within_at_Ioc_iff_Iic {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_closed_topology α] [topological_space β] {a b : α} {f : α → β} (h : a < b) :
theorem frontier_le_subset_eq {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_closed_topology α] {f g : β → α} [topological_space β] (hf : continuous f) (hg : continuous g) :
frontier {b : β | f b g b} {b : β | f b = g b}
theorem frontier_Iic_subset {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] (a : α) :
theorem frontier_Ici_subset {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] (a : α) :
theorem frontier_lt_subset_eq {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_closed_topology α] {f g : β → α} [topological_space β] (hf : continuous f) (hg : continuous g) :
frontier {b : β | f b < g b} {b : β | f b = g b}
theorem continuous_if_le {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] {f g : β → α} [topological_space β] [topological_space γ] [Π (x : β), decidable (f x g x)] {f' g' : β → γ} (hf : continuous f) (hg : continuous g) (hf' : continuous_on f' {x : β | f x g x}) (hg' : continuous_on g' {x : β | g x f x}) (hfg : ∀ (x : β), f x = g xf' x = g' x) :
continuous (λ (x : β), ite (f x g x) (f' x) (g' x))
theorem continuous.if_le {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [linear_order α] [order_closed_topology α] {f g : β → α} [topological_space β] [topological_space γ] [Π (x : β), decidable (f x g x)] {f' g' : β → γ} (hf' : continuous f') (hg' : continuous g') (hf : continuous f) (hg : continuous g) (hfg : ∀ (x : β), f x = g xf' x = g' x) :
continuous (λ (x : β), ite (f x g x) (f' x) (g' x))
@[continuity]
theorem continuous.min {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_closed_topology α] {f g : β → α} [topological_space β] (hf : continuous f) (hg : continuous g) :
continuous (λ (b : β), min (f b) (g b))
@[continuity]
theorem continuous.max {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_closed_topology α] {f g : β → α} [topological_space β] (hf : continuous f) (hg : continuous g) :
continuous (λ (b : β), max (f b) (g b))
theorem continuous_min {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] :
continuous (λ (p : α × α), min p.fst p.snd)
theorem continuous_max {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] :
continuous (λ (p : α × α), max p.fst p.snd)
theorem filter.tendsto.max {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_closed_topology α] {f g : β → α} {b : filter β} {a₁ a₂ : α} (hf : filter.tendsto f b (𝓝 a₁)) (hg : filter.tendsto g b (𝓝 a₂)) :
filter.tendsto (λ (b : β), max (f b) (g b)) b (𝓝 (max a₁ a₂))
theorem filter.tendsto.min {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_closed_topology α] {f g : β → α} {b : filter β} {a₁ a₂ : α} (hf : filter.tendsto f b (𝓝 a₁)) (hg : filter.tendsto g b (𝓝 a₂)) :
filter.tendsto (λ (b : β), min (f b) (g b)) b (𝓝 (min a₁ a₂))
@[class]
structure order_topology (α : Type u_1) [t : topological_space α] [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.

Instances
def preorder.topology (α : Type u_1) [preorder α] :

(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
@[protected, instance]
theorem is_open_iff_generate_intervals {α : Type u} [topological_space α] [partial_order α] [t : order_topology α] {s : set α} :
is_open s topological_space.generate_open {s : set α | ∃ (a : α), s = set.Ioi a s = set.Iio a} s
theorem is_open_lt' {α : Type u} [topological_space α] [partial_order α] [t : order_topology α] (a : α) :
is_open {b : α | a < b}
theorem is_open_gt' {α : Type u} [topological_space α] [partial_order α] [t : order_topology α] (a : α) :
is_open {b : α | b < a}
theorem lt_mem_nhds {α : Type u} [topological_space α] [partial_order α] [t : order_topology α] {a b : α} (h : a < b) :
∀ᶠ (x : α) in 𝓝 b, a < x
theorem le_mem_nhds {α : Type u} [topological_space α] [partial_order α] [t : order_topology α] {a b : α} (h : a < b) :
∀ᶠ (x : α) in 𝓝 b, a x
theorem gt_mem_nhds {α : Type u} [topological_space α] [partial_order α] [t : order_topology α] {a b : α} (h : a < b) :
∀ᶠ (x : α) in 𝓝 a, x < b
theorem ge_mem_nhds {α : Type u} [topological_space α] [partial_order α] [t : order_topology α] {a b : α} (h : a < b) :
∀ᶠ (x : α) in 𝓝 a, x b
theorem nhds_eq_order {α : Type u} [topological_space α] [partial_order α] [t : order_topology α] (a : α) :
𝓝 a = (⨅ (b : α) (H : b set.Iio a), 𝓟 (set.Ioi b)) ⨅ (b : α) (H : b set.Ioi a), 𝓟 (set.Iio b)
theorem tendsto_order {α : Type u} {β : Type v} [topological_space α] [partial_order α] [t : order_topology α] {f : β → α} {a : α} {x : filter β} :
filter.tendsto f x (𝓝 a) (∀ (a' : α), a' < a(∀ᶠ (b : β) in x, a' < f b)) ∀ (a' : α), a' > a(∀ᶠ (b : β) in x, f b < a')
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem tendsto_of_tendsto_of_tendsto_of_le_of_le' {α : Type u} {β : Type v} [topological_space α] [partial_order α] [t : order_topology α] {f g h : β → α} {b : filter β} {a : α} (hg : filter.tendsto g b (𝓝 a)) (hh : filter.tendsto h b (𝓝 a)) (hgf : ∀ᶠ (b : β) in b, g b f b) (hfh : ∀ᶠ (b : β) in b, f b h b) :

Also known as squeeze or 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} [topological_space α] [partial_order α] [t : order_topology α] {f g h : β → α} {b : filter β} {a : α} (hg : filter.tendsto g b (𝓝 a)) (hh : filter.tendsto h b (𝓝 a)) (hgf : g f) (hfh : f h) :

Also known as squeeze or sandwich theorem. This version assumes that inequalities hold everywhere.

theorem nhds_order_unbounded {α : Type u} [topological_space α] [partial_order α] [t : order_topology α] {a : α} (hu : ∃ (u : α), a < u) (hl : ∃ (l : α), l < a) :
𝓝 a = ⨅ (l : α) (h₂ : l < a) (u : α) (h₂ : a < u), 𝓟 (set.Ioo l u)
theorem tendsto_order_unbounded {α : Type u} {β : Type v} [topological_space α] [partial_order α] [t : order_topology α] {f : β → α} {a : α} {x : filter β} (hu : ∃ (u : α), a < u) (hl : ∃ (l : α), l < a) (h : ∀ (l u : α), l < aa < u(∀ᶠ (b : β) in x, l < f b f b < u)) :
@[protected, instance]
def tendsto_Ixx_nhds_within {α : Type u_1} [preorder α] [topological_space α] (a : α) {s t : set α} {Ixx : α → α → set α} [filter.tendsto_Ixx_class Ixx (𝓝 a) (𝓝 a)] [filter.tendsto_Ixx_class Ixx (𝓟 s) (𝓟 t)] :
@[protected, instance]
def tendsto_Icc_class_nhds_pi {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), partial_order (α i)] [Π (i : ι), topological_space (α i)] [∀ (i : ι), order_topology (α i)] (f : Π (i : ι), α i) :
theorem induced_order_topology' {α : Type u} {β : Type v} [partial_order α] [ta : topological_space β] [partial_order β] [order_topology β] (f : α → β) (hf : ∀ {x y : α}, f x < f y x < y) (H₁ : ∀ {a : α} {x : β}, x < f a(∃ (b : α) (H : b < a), x f b)) (H₂ : ∀ {a : α} {x : β}, f a < x(∃ (b : α) (H : b > a), f b x)) :
theorem induced_order_topology {α : Type u} {β : Type v} [partial_order α] [ta : topological_space β] [partial_order β] [order_topology β] (f : α → β) (hf : ∀ {x y : α}, f x < f y x < y) (H : ∀ {x y : β}, x < y(∃ (a : α), x < f a f a < y)) :
@[protected, instance]

On an ord_connected 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.

theorem nhds_top_order {α : Type u} [topological_space α] [order_top α] [order_topology α] :
𝓝 = ⨅ (l : α) (h₂ : l < ), 𝓟 (set.Ioi l)
theorem nhds_bot_order {α : Type u} [topological_space α] [order_bot α] [order_topology α] :
𝓝 = ⨅ (l : α) (h₂ : < l), 𝓟 (set.Iio l)
theorem tendsto_nhds_top_mono {α : Type u} {β : Type v} [topological_space β] [order_top β] [order_topology β] {l : filter α} {f g : α → β} (hf : filter.tendsto f l (𝓝 )) (hg : f ≤ᶠ[l] g) :
theorem tendsto_nhds_bot_mono {α : Type u} {β : Type v} [topological_space β] [order_bot β] [order_topology β] {l : filter α} {f g : α → β} (hf : filter.tendsto f l (𝓝 )) (hg : g ≤ᶠ[l] f) :
theorem tendsto_nhds_top_mono' {α : Type u} {β : Type v} [topological_space β] [order_top β] [order_topology β] {l : filter α} {f g : α → β} (hf : filter.tendsto f l (𝓝 )) (hg : f g) :
theorem tendsto_nhds_bot_mono' {α : Type u} {β : Type v} [topological_space β] [order_bot β] [order_topology β] {l : filter α} {f g : α → β} (hf : filter.tendsto f l (𝓝 )) (hg : g f) :
theorem exists_Ioc_subset_of_mem_nhds' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (hs : s 𝓝 a) {l : α} (hl : l < a) :
∃ (l' : α) (H : l' set.Ico l a), set.Ioc l' a s
theorem exists_Ico_subset_of_mem_nhds' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (hs : s 𝓝 a) {u : α} (hu : a < u) :
∃ (u' : α) (H : u' set.Ioc a u), set.Ico a u' s
theorem exists_Ioc_subset_of_mem_nhds {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (hs : s 𝓝 a) (h : ∃ (l : α), l < a) :
∃ (l : α) (H : l < a), set.Ioc l a s
theorem exists_Ico_subset_of_mem_nhds {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (hs : s 𝓝 a) (h : ∃ (u : α), a < u) :
∃ (u : α) (_x : a < u), set.Ico a u s
theorem order_separated {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a₁ a₂ : α} (h : a₁ < a₂) :
∃ (u v : set α), is_open u is_open v a₁ u a₂ v ∀ (b₁ : α), b₁ u∀ (b₂ : α), b₂ vb₁ < b₂
@[protected, instance]
theorem mem_nhds_iff_exists_Ioo_subset' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (hl : ∃ (l : α), l < a) (hu : ∃ (u : α), a < u) :
s 𝓝 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} [topological_space α] [linear_order α] [order_topology α] [no_top_order α] [no_bot_order α] {a : α} {s : set α} :
s 𝓝 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} [topological_space α] [linear_order α] [order_topology α] {a : α} (hl : ∃ (l : α), l < a) (hu : ∃ (u : α), a < u) :
(𝓝 a).has_basis (λ (b : α × α), b.fst < a a < b.snd) (λ (b : α × α), set.Ioo b.fst b.snd)
theorem nhds_basis_Ioo {α : Type u} [topological_space α] [linear_order α] [order_topology α] [no_top_order α] [no_bot_order α] {a : α} :
(𝓝 a).has_basis (λ (b : α × α), b.fst < a a < b.snd) (λ (b : α × α), set.Ioo b.fst b.snd)
theorem filter.eventually.exists_Ioo_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] [no_top_order α] [no_bot_order α] {a : α} {p : α → Prop} (hp : ∀ᶠ (x : α) in 𝓝 a, p x) :
∃ (l u : α), a set.Ioo l u set.Ioo l u {x : α | p x}
theorem Iio_mem_nhds {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a b : α} (h : a < b) :
theorem Ioi_mem_nhds {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a b : α} (h : a < b) :
theorem Iic_mem_nhds {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a b : α} (h : a < b) :
theorem Ici_mem_nhds {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a b : α} (h : a < b) :
theorem Ioo_mem_nhds {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a b x : α} (ha : a < x) (hb : x < b) :
theorem Ioc_mem_nhds {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a b x : α} (ha : a < x) (hb : x < b) :
theorem Ico_mem_nhds {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a b x : α} (ha : a < x) (hb : x < b) :
theorem Icc_mem_nhds {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a b x : α} (ha : a < x) (hb : x < b) :

Intervals in Π i, π i belong to 𝓝 x #

For each leamma 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} [fintype ι] [Π (i : ι), linear_order («π» i)] [Π (i : ι), topological_space («π» i)] [∀ (i : ι), order_topology («π» i)] {a x : Π (i : ι), «π» i} (ha : ∀ (i : ι), x i < a i) :
theorem pi_Iic_mem_nhds' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {ι : Type u_1} [fintype ι] {a' x' : ι → α} (ha : ∀ (i : ι), x' i < a' i) :
theorem pi_Ici_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [fintype ι] [Π (i : ι), linear_order («π» i)] [Π (i : ι), topological_space («π» i)] [∀ (i : ι), order_topology («π» i)] {a x : Π (i : ι), «π» i} (ha : ∀ (i : ι), a i < x i) :
theorem pi_Ici_mem_nhds' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {ι : Type u_1} [fintype ι] {a' x' : ι → α} (ha : ∀ (i : ι), a' i < x' i) :
theorem pi_Icc_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [fintype ι] [Π (i : ι), linear_order («π» i)] [Π (i : ι), topological_space («π» i)] [∀ (i : ι), order_topology («π» i)] {a b x : Π (i : ι), «π» i} (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
theorem pi_Icc_mem_nhds' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {ι : Type u_1} [fintype ι] {a' b' x' : ι → α} (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
set.Icc a' b' 𝓝 x'
theorem pi_Iio_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [fintype ι] [Π (i : ι), linear_order («π» i)] [Π (i : ι), topological_space («π» i)] [∀ (i : ι), order_topology («π» i)] {a x : Π (i : ι), «π» i} [nonempty ι] (ha : ∀ (i : ι), x i < a i) :
theorem pi_Iio_mem_nhds' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {ι : Type u_1} [fintype ι] {a' x' : ι → α} [nonempty ι] (ha : ∀ (i : ι), x' i < a' i) :
theorem pi_Ioi_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [fintype ι] [Π (i : ι), linear_order («π» i)] [Π (i : ι), topological_space («π» i)] [∀ (i : ι), order_topology («π» i)] {a x : Π (i : ι), «π» i} [nonempty ι] (ha : ∀ (i : ι), a i < x i) :
theorem pi_Ioi_mem_nhds' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {ι : Type u_1} [fintype ι] {a' x' : ι → α} [nonempty ι] (ha : ∀ (i : ι), a' i < x' i) :
theorem pi_Ioc_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [fintype ι] [Π (i : ι), linear_order («π» i)] [Π (i : ι), topological_space («π» i)] [∀ (i : ι), order_topology («π» i)] {a b x : Π (i : ι), «π» i} [nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
theorem pi_Ioc_mem_nhds' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {ι : Type u_1} [fintype ι] {a' b' x' : ι → α} [nonempty ι] (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
set.Ioc a' b' 𝓝 x'
theorem pi_Ico_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [fintype ι] [Π (i : ι), linear_order («π» i)] [Π (i : ι), topological_space («π» i)] [∀ (i : ι), order_topology («π» i)] {a b x : Π (i : ι), «π» i} [nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
theorem pi_Ico_mem_nhds' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {ι : Type u_1} [fintype ι] {a' b' x' : ι → α} [nonempty ι] (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
set.Ico a' b' 𝓝 x'
theorem pi_Ioo_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [fintype ι] [Π (i : ι), linear_order («π» i)] [Π (i : ι), topological_space («π» i)] [∀ (i : ι), order_topology («π» i)] {a b x : Π (i : ι), «π» i} [nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
theorem pi_Ioo_mem_nhds' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {ι : Type u_1} [fintype ι] {a' b' x' : ι → α} [nonempty ι] (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
set.Ioo a' b' 𝓝 x'
@[simp]
theorem inf_nhds_at_top {α : Type u} [topological_space α] [linear_order α] [order_topology α] [no_top_order α] (x : α) :
@[simp]
theorem inf_nhds_at_bot {α : Type u} [topological_space α] [linear_order α] [order_topology α] [no_bot_order α] (x : α) :
theorem not_tendsto_nhds_of_tendsto_at_top {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_topology α] [no_top_order α] {F : filter β} [F.ne_bot] {f : β → α} (hf : filter.tendsto f F filter.at_top) (x : α) :
theorem not_tendsto_at_top_of_tendsto_nhds {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_topology α] [no_top_order α] {F : filter β} [F.ne_bot] {f : β → α} {x : α} (hf : filter.tendsto f F (𝓝 x)) :
theorem not_tendsto_nhds_of_tendsto_at_bot {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_topology α] [no_bot_order α] {F : filter β} [F.ne_bot] {f : β → α} (hf : filter.tendsto f F filter.at_bot) (x : α) :
theorem not_tendsto_at_bot_of_tendsto_nhds {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_topology α] [no_bot_order α] {F : filter β} [F.ne_bot] {f : β → α} {x : α} (hf : filter.tendsto f F (𝓝 x)) :

Neighborhoods to the left and to the right on an order_topology #

We've seen some properties of left and right neighborhood of a point in an order_closed_topology. In an order_topology, 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_nhds_within_Ioi {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a b : α} (hab : a < b) (s : set α) :
[s 𝓝[set.Ioi a] a, s 𝓝[set.Ioc a b] a, s 𝓝[set.Ioo a b] a, ∃ (u : α) (H : u set.Ioc a b), set.Ioo a u s, ∃ (u : α) (H : u set.Ioi a), set.Ioo a u s].tfae

The following statements are equivalent:

  1. s is a neighborhood of a within (a, +∞)
  2. s is a neighborhood of a within (a, b]
  3. s is a neighborhood of a within (a, b)
  4. s includes (a, u) for some u ∈ (a, b]
  5. s includes (a, u) for some u > a
theorem mem_nhds_within_Ioi_iff_exists_mem_Ioc_Ioo_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a u' : α} {s : set α} (hu' : a < u') :
s 𝓝[set.Ioi a] a ∃ (u : α) (H : u set.Ioc a u'), set.Ioo a u s
theorem mem_nhds_within_Ioi_iff_exists_Ioo_subset' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a u' : α} {s : set α} (hu' : a < u') :
s 𝓝[set.Ioi a] a ∃ (u : α) (H : 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 mem_nhds_within_Ioi_iff_exists_Ioo_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] [no_top_order α] {a : α} {s : set α} :
s 𝓝[set.Ioi a] a ∃ (u : α) (H : 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 mem_nhds_within_Ioi_iff_exists_Ioc_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] [no_top_order α] [densely_ordered α] {a : α} {s : set α} :
s 𝓝[set.Ioi a] a ∃ (u : α) (H : 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_nhds_within_Iio {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a b : α} (h : a < b) (s : set α) :
[s 𝓝[set.Iio b] b, s 𝓝[set.Ico a b] b, s 𝓝[set.Ioo a b] b, ∃ (l : α) (H : l set.Ico a b), set.Ioo l b s, ∃ (l : α) (H : l set.Iio b), set.Ioo l b s].tfae

The following statements are equivalent:

  1. s is a neighborhood of b within (-∞, b)
  2. s is a neighborhood of b within [a, b)
  3. s is a neighborhood of b within (a, b)
  4. s includes (l, b) for some l ∈ [a, b)
  5. s includes (l, b) for some l < b
theorem mem_nhds_within_Iio_iff_exists_mem_Ico_Ioo_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a l' : α} {s : set α} (hl' : l' < a) :
s 𝓝[set.Iio a] a ∃ (l : α) (H : l set.Ico l' a), set.Ioo l a s
theorem mem_nhds_within_Iio_iff_exists_Ioo_subset' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a l' : α} {s : set α} (hl' : l' < a) :
s 𝓝[set.Iio a] a ∃ (l : α) (H : 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_nhds_within_Iio_iff_exists_Ioo_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] [no_bot_order α] {a : α} {s : set α} :
s 𝓝[set.Iio a] a ∃ (l : α) (H : 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_nhds_within_Iio_iff_exists_Ico_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] [no_bot_order α] [densely_ordered α] {a : α} {s : set α} :
s 𝓝[set.Iio a] a ∃ (l : α) (H : 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 tfae_mem_nhds_within_Ici {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a b : α} (hab : a < b) (s : set α) :
[s 𝓝[set.Ici a] a, s 𝓝[set.Icc a b] a, s 𝓝[set.Ico a b] a, ∃ (u : α) (H : u set.Ioc a b), set.Ico a u s, ∃ (u : α) (H : u set.Ioi a), set.Ico a u s].tfae

The following statements are equivalent:

  1. s is a neighborhood of a within [a, +∞)
  2. s is a neighborhood of a within [a, b]
  3. s is a neighborhood of a within [a, b)
  4. s includes [a, u) for some u ∈ (a, b]
  5. s includes [a, u) for some u > a
theorem mem_nhds_within_Ici_iff_exists_mem_Ioc_Ico_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a u' : α} {s : set α} (hu' : a < u') :
s 𝓝[set.Ici a] a ∃ (u : α) (H : u set.Ioc a u'), set.Ico a u s
theorem mem_nhds_within_Ici_iff_exists_Ico_subset' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a u' : α} {s : set α} (hu' : a < u') :
s 𝓝[set.Ici a] a ∃ (u : α) (H : 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_nhds_within_Ici_iff_exists_Ico_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] [no_top_order α] {a : α} {s : set α} :
s 𝓝[set.Ici a] a ∃ (u : α) (H : 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 mem_nhds_within_Ici_iff_exists_Icc_subset' {α : Type u} [topological_space α] [linear_order α] [order_topology α] [no_top_order α] [densely_ordered α] {a : α} {s : set α} :
s 𝓝[set.Ici a] a ∃ (u : α) (H : u set.Ioi a), 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_nhds_within_Iic {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a b : α} (h : a < b) (s : set α) :
[s 𝓝[set.Iic b] b, s 𝓝[set.Icc a b] b, s 𝓝[set.Ioc a b] b, ∃ (l : α) (H : l set.Ico a b), set.Ioc l b s, ∃ (l : α) (H : l set.Iio b), set.Ioc l b s].tfae

The following statements are equivalent:

  1. s is a neighborhood of b within (-∞, b]
  2. s is a neighborhood of b within [a, b]
  3. s is a neighborhood of b within (a, b]
  4. s includes (l, b] for some l ∈ [a, b)
  5. s includes (l, b] for some l < b
theorem mem_nhds_within_Iic_iff_exists_mem_Ico_Ioc_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a l' : α} {s : set α} (hl' : l' < a) :
s 𝓝[set.Iic a] a ∃ (l : α) (H : l set.Ico l' a), set.Ioc l a s
theorem mem_nhds_within_Iic_iff_exists_Ioc_subset' {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a l' : α} {s : set α} (hl' : l' < a) :
s 𝓝[set.Iic a] a ∃ (l : α) (H : 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_nhds_within_Iic_iff_exists_Ioc_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] [no_bot_order α] {a : α} {s : set α} :
s 𝓝[set.Iic a] a ∃ (l : α) (H : 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_nhds_within_Iic_iff_exists_Icc_subset' {α : Type u} [topological_space α] [linear_order α] [order_topology α] [no_bot_order α] [densely_ordered α] {a : α} {s : set α} :
s 𝓝[set.Iic a] a ∃ (l : α) (H : l set.Iio 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 mem_nhds_within_Ici_iff_exists_Icc_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] [no_top_order α] [densely_ordered α] {a : α} {s : set α} :
s 𝓝[set.Ici a] 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 mem_nhds_within_Iic_iff_exists_Icc_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] [no_bot_order α] [densely_ordered α] {a : α} {s : set α} :
s 𝓝[set.Iic a] a ∃ (l : α), 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 nhds_eq_infi_abs_sub {α : Type u} [topological_space α] [linear_ordered_add_comm_group α] [order_topology α] (a : α) :
𝓝 a = ⨅ (r : α) (H : r > 0), 𝓟 {b : α | abs (a - b) < r}
theorem order_topology_of_nhds_abs {α : Type u_1} [topological_space α] [linear_ordered_add_comm_group α] (h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α) (H : r > 0), 𝓟 {b : α | abs (a - b) < r}) :
theorem linear_ordered_add_comm_group.tendsto_nhds {α : Type u} {β : Type v} [topological_space α] [linear_ordered_add_comm_group α] [order_topology α] {f : β → α} {x : filter β} {a : α} :
filter.tendsto f x (𝓝 a) ∀ (ε : α), ε > 0(∀ᶠ (b : β) in x, abs (f b - a) < ε)
theorem eventually_abs_sub_lt {α : Type u} [topological_space α] [linear_ordered_add_comm_group α] [order_topology α] (a : α) {ε : α} (hε : 0 < ε) :
∀ᶠ (x : α) in 𝓝 a, abs (x - a) < ε
@[continuity]
theorem filter.tendsto.abs {α : Type u} {β : Type v} [topological_space α] [linear_ordered_add_comm_group α] [order_topology α] {f : β → α} {a : α} {l : filter β} (h : filter.tendsto f l (𝓝 a)) :
filter.tendsto (λ (x : β), abs (f x)) l (𝓝 (abs a))
theorem continuous.abs {α : Type u} {β : Type v} [topological_space α] [linear_ordered_add_comm_group α] [order_topology α] {f : β → α} [topological_space β] (h : continuous f) :
continuous (λ (x : β), abs (f x))
theorem continuous_at.abs {α : Type u} {β : Type v} [topological_space α] [linear_ordered_add_comm_group α] [order_topology α] {f : β → α} [topological_space β] {b : β} (h : continuous_at f b) :
continuous_at (λ (x : β), abs (f x)) b
theorem continuous_within_at.abs {α : Type u} {β : Type v} [topological_space α] [linear_ordered_add_comm_group α] [order_topology α] {f : β → α} [topological_space β] {b : β} {s : set β} (h : continuous_within_at f s b) :
continuous_within_at (λ (x : β), abs (f x)) s b
theorem continuous_on.abs {α : Type u} {β : Type v} [topological_space α] [linear_ordered_add_comm_group α] [order_topology α] {f : β → α} [topological_space β] {s : set β} (h : continuous_on f s) :
continuous_on (λ (x : β), abs (f x)) s
theorem filter.tendsto.add_at_top {α : Type u} {β : Type v} [topological_space α] [linear_ordered_add_comm_group α] [order_topology α] {l : filter β} {f g : β → α} {C : α} (hf : filter.tendsto f l (𝓝 C)) (hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : β), f x + g x) l filter.at_top

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

theorem filter.tendsto.add_at_bot {α : Type u} {β : Type v} [topological_space α] [linear_ordered_add_comm_group α] [order_topology α] {l : filter β} {f g : β → α} {C : α} (hf : filter.tendsto f l (𝓝 C)) (hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : β), f x + g x) l filter.at_bot

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

theorem filter.tendsto.at_top_add {α : Type u} {β : Type v} [topological_space α] [linear_ordered_add_comm_group α] [order_topology α] {l : filter β} {f g : β → α} {C : α} (hf : filter.tendsto f l filter.at_top) (hg : filter.tendsto g l (𝓝 C)) :
filter.tendsto (λ (x : β), f x + g x) l filter.at_top

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

theorem filter.tendsto.at_bot_add {α : Type u} {β : Type v} [topological_space α] [linear_ordered_add_comm_group α] [order_topology α] {l : filter β} {f g : β → α} {C : α} (hf : filter.tendsto f l filter.at_bot) (hg : filter.tendsto g l (𝓝 C)) :
filter.tendsto (λ (x : β), f x + g x) l filter.at_bot

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

theorem filter.tendsto.at_top_mul {α : Type u} {β : Type v} [linear_ordered_field α] [topological_space α] [order_topology α] {l : filter β} {f g : β → α} {C : α} (hC : 0 < C) (hf : filter.tendsto f l filter.at_top) (hg : filter.tendsto g l (𝓝 C)) :
filter.tendsto (λ (x : β), (f x) * g x) l filter.at_top

In a linearly ordered field with the order topology, if f tends to at_top and g tends to a positive constant C then f * g tends to at_top.

theorem filter.tendsto.mul_at_top {α : Type u} {β : Type v} [linear_ordered_field α] [topological_space α] [order_topology α] {l : filter β} {f g : β → α} {C : α} (hC : 0 < C) (hf : filter.tendsto f l (𝓝 C)) (hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : β), (f x) * g x) l filter.at_top

In a linearly ordered field with the order topology, if f tends to a positive constant C and g tends to at_top then f * g tends to at_top.

theorem filter.tendsto.at_top_mul_neg {α : Type u} {β : Type v} [linear_ordered_field α] [topological_space α] [order_topology α] {l : filter β} {f g : β → α} {C : α} (hC : C < 0) (hf : filter.tendsto f l filter.at_top) (hg : filter.tendsto g l (𝓝 C)) :
filter.tendsto (λ (x : β), (f x) * g x) l filter.at_bot

In a linearly ordered field with the order topology, if f tends to at_top and g tends to a negative constant C then f * g tends to at_bot.

theorem filter.tendsto.neg_mul_at_top {α : Type u} {β : Type v} [linear_ordered_field α] [topological_space α] [order_topology α] {l : filter β} {f g : β → α} {C : α} (hC : C < 0) (hf : filter.tendsto f l (𝓝 C)) (hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : β), (f x) * g x) l filter.at_bot

In a linearly ordered field with the order topology, if f tends to a negative constant C and g tends to at_top then f * g tends to at_bot.

theorem filter.tendsto.at_bot_mul {α : Type u} {β : Type v} [linear_ordered_field α] [topological_space α] [order_topology α] {l : filter β} {f g : β → α} {C : α} (hC : 0 < C) (hf : filter.tendsto f l filter.at_bot) (hg : filter.tendsto g l (𝓝 C)) :
filter.tendsto (λ (x : β), (f x) * g x) l filter.at_bot

In a linearly ordered field with the order topology, if f tends to at_bot and g tends to a positive constant C then f * g tends to at_bot.

theorem filter.tendsto.at_bot_mul_neg {α : Type u} {β : Type v} [linear_ordered_field α] [topological_space α] [order_topology α] {l : filter β} {f g : β → α} {C : α} (hC : C < 0) (hf : filter.tendsto f l filter.at_bot) (hg : filter.tendsto g l (𝓝 C)) :
filter.tendsto (λ (x : β), (f x) * g x) l filter.at_top

In a linearly ordered field with the order topology, if f tends to at_bot and g tends to a negative constant C then f * g tends to at_top.

theorem filter.tendsto.mul_at_bot {α : Type u} {β : Type v} [linear_ordered_field α] [topological_space α] [order_topology α] {l : filter β} {f g : β → α} {C : α} (hC : 0 < C) (hf : filter.tendsto f l (𝓝 C)) (hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : β), (f x) * g x) l filter.at_bot

In a linearly ordered field with the order topology, if f tends to a positive constant C and g tends to at_bot then f * g tends to at_bot.

theorem filter.tendsto.neg_mul_at_bot {α : Type u} {β : Type v} [linear_ordered_field α] [topological_space α] [order_topology α] {l : filter β} {f g : β → α} {C : α} (hC : C < 0) (hf : filter.tendsto f l (𝓝 C)) (hg : filter.tendsto g l filter.at_bot) :
filter.tendsto (λ (x : β), (f x) * g x) l filter.at_top

In a linearly ordered field with the order topology, if f tends to a negative constant C and g tends to at_bot then f * g tends to at_top.

The function x ↦ x⁻¹ tends to +∞ on the right of 0.

The function r ↦ r⁻¹ tends to 0 on the right as r → +∞.

theorem filter.tendsto.div_at_top {α : Type u} {β : Type v} [linear_ordered_field α] [topological_space α] [order_topology α] [has_continuous_mul α] {f g : β → α} {l : filter β} {a : α} (h : filter.tendsto f l (𝓝 a)) (hg : filter.tendsto g l filter.at_top) :
filter.tendsto (λ (x : β), f x / g x) l (𝓝 0)
theorem filter.tendsto.inv_tendsto_at_top {α : Type u} {β : Type v} [linear_ordered_field α] [topological_space α] [order_topology α] {l : filter β} {f : β → α} (h : filter.tendsto f l filter.at_top) :
theorem filter.tendsto.inv_tendsto_zero {α : Type u} {β : Type v} [linear_ordered_field α] [topological_space α] [order_topology α] {l : filter β} {f : β → α} (h : filter.tendsto f l (𝓝[set.Ioi 0] 0)) :
theorem tendsto_pow_neg_at_top {α : Type u} [linear_ordered_field α] [topological_space α] [order_topology α] {n : } (hn : 1 n) :
filter.tendsto (λ (x : α), x ^ -n) filter.at_top (𝓝 0)

The function x^(-n) tends to 0 at +∞ for any positive natural n. A version for positive real powers exists as tendsto_rpow_neg_at_top.

theorem tendsto_fpow_at_top_zero {α : Type u} [linear_ordered_field α] [topological_space α] [order_topology α] {n : } (hn : n < 0) :
filter.tendsto (λ (x : α), x ^ n) filter.at_top (𝓝 0)
theorem is_lub.frequently_mem {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (ha : is_lub s a) (hs : s.nonempty) :
∃ᶠ (x : α) in 𝓝[set.Iic a] a, x s
theorem is_lub.frequently_nhds_mem {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (ha : is_lub s a) (hs : s.nonempty) :
∃ᶠ (x : α) in 𝓝 a, x s
theorem is_glb.frequently_mem {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (ha : is_glb s a) (hs : s.nonempty) :
∃ᶠ (x : α) in 𝓝[set.Ici a] a, x s
theorem is_glb.frequently_nhds_mem {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (ha : is_glb s a) (hs : s.nonempty) :
∃ᶠ (x : α) in 𝓝 a, x s
theorem is_lub.mem_closure {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (ha : is_lub s a) (hs : s.nonempty) :
theorem is_glb.mem_closure {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (ha : is_glb s a) (hs : s.nonempty) :
theorem is_lub.nhds_within_ne_bot {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (ha : is_lub s a) (hs : s.nonempty) :
theorem is_glb.nhds_within_ne_bot {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} :
is_glb s as.nonempty(𝓝[s] a).ne_bot
theorem is_lub_of_mem_nhds {α : Type u} [topological_space α] [linear_order α] [order_topology α] {s : set α} {a : α} {f : filter α} (hsa : a upper_bounds s) (hsf : s f) [(f 𝓝 a).ne_bot] :
is_lub s a
theorem is_glb_of_mem_nhds {α : Type u} [topological_space α] [linear_order α] [order_topology α] {s : set α} {a : α} {f : filter α} :
a lower_bounds ss f(f 𝓝 a).ne_botis_glb s a
theorem is_lub.mem_upper_bounds_of_tendsto {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_topology α] [preorder γ] [topological_space γ] [order_closed_topology γ] {f : α → γ} {s : set α} {a : α} {b : γ} (hf : ∀ (x : α), x s∀ (y : α), y sx yf x f y) (ha : is_lub s a) (hb : filter.tendsto f (𝓝[s] a) (𝓝 b)) :
theorem is_lub.is_lub_of_tendsto {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_topology α] [preorder γ] [topological_space γ] [order_closed_topology γ] {f : α → γ} {s : set α} {a : α} {b : γ} (hf : ∀ (x : α), x s∀ (y : α), y sx yf x f y) (ha : is_lub s a) (hs : s.nonempty) (hb : filter.tendsto f (𝓝[s] a) (𝓝 b)) :
is_lub (f '' s) b
theorem is_glb.mem_lower_bounds_of_tendsto {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_topology α] [preorder γ] [topological_space γ] [order_closed_topology γ] {f : α → γ} {s : set α} {a : α} {b : γ} (hf : ∀ (x : α), x s∀ (y : α), y sx yf x f y) (ha : is_glb s a) (hb : filter.tendsto f (𝓝[s] a) (𝓝 b)) :
theorem is_glb.is_glb_of_tendsto {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_topology α] [preorder γ] [topological_space γ] [order_closed_topology γ] {f : α → γ} {s : set α} {a : α} {b : γ} (hf : ∀ (x : α), x s∀ (y : α), y sx yf x f y) :
is_glb s as.nonemptyfilter.tendsto f (𝓝[s] a) (𝓝 b)is_glb (f '' s) b
theorem is_lub.mem_lower_bounds_of_tendsto {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_topology α] [preorder γ] [topological_space γ] [order_closed_topology γ] {f : α → γ} {s : set α} {a : α} {b : γ} (hf : ∀ (x : α), x s∀ (y : α), y sx yf y f x) (ha : is_lub s a) (hb : filter.tendsto f (𝓝[s] a) (𝓝 b)) :
theorem is_lub.is_glb_of_tendsto {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_topology α] [preorder γ] [topological_space γ] [order_closed_topology γ] {f : α → γ} {s : set α} {a : α} {b : γ} :
(∀ (x : α), x s∀ (y : α), y sx yf y f x)is_lub s as.nonemptyfilter.tendsto f (𝓝[s] a) (𝓝 b)is_glb (f '' s) b
theorem is_glb.mem_upper_bounds_of_tendsto {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_topology α] [preorder γ] [topological_space γ] [order_closed_topology γ] {f : α → γ} {s : set α} {a : α} {b : γ} (hf : ∀ (x : α), x s∀ (y : α), y sx yf y f x) (ha : is_glb s a) (hb : filter.tendsto f (𝓝[s] a) (𝓝 b)) :
theorem is_glb.is_lub_of_tendsto {α : Type u} {γ : Type w} [topological_space α] [linear_order α] [order_topology α] [preorder γ] [topological_space γ] [order_closed_topology γ] {f : α → γ} {s : set α} {a : α} {b : γ} :
(∀ (x : α), x s∀ (y : α), y sx yf y f x)is_glb s as.nonemptyfilter.tendsto f (𝓝[s] a) (𝓝 b)is_lub (f '' s) b
theorem is_lub.mem_of_is_closed {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (ha : is_lub s a) (hs : s.nonempty) (sc : is_closed s) :
a s
theorem is_closed.is_lub_mem {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (ha : is_lub s a) (hs : s.nonempty) (sc : is_closed s) :
a s

Alias of is_lub.mem_of_is_closed.

theorem is_glb.mem_of_is_closed {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (ha : is_glb s a) (hs : s.nonempty) (sc : is_closed s) :
a s
theorem is_closed.is_glb_mem {α : Type u} [topological_space α] [linear_order α] [order_topology α] {a : α} {s : set α} (ha : is_glb s a) (hs : s.nonempty) (sc : is_closed s) :
a s

Alias of is_glb.mem_of_is_closed.

theorem is_compact.bdd_below {α : Type u} [topological_space α] [linear_order α] [order_closed_topology α] [nonempty α] {s : set α} (hs : is_compact s) :

A compact set is bounded below

theorem is_compact.bdd_above {α : Type u} [topological_space α] [linear_order α] [order_topology α] [nonempty α] {s : set α} :

A compact set is bounded above

theorem closure_Ioi' {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} (hab : a < b) :

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

@[simp]
theorem closure_Ioi {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] (a : α) [no_top_order α] :

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

theorem closure_Iio' {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} (hab : b < a) :

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

@[simp]
theorem closure_Iio {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] (a : α) [no_bot_order α] :

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

@[simp]
theorem closure_Ioo {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} (hab : a < b) :

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

@[simp]
theorem closure_Ioc {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} (hab : a < b) :

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

@[simp]
theorem closure_Ico {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} (hab : a < b) :

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

@[simp]
theorem interior_Ici {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] [no_bot_order α] {a : α} :
@[simp]
theorem interior_Iic {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] [no_top_order α] {a : α} :
@[simp]
theorem interior_Icc {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] [no_bot_order α] [no_top_order α] {a b : α} :
@[simp]
theorem interior_Ico {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] [no_bot_order α] {a b : α} :
@[simp]
theorem interior_Ioc {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] [no_top_order α] {a b : α} :
@[simp]
theorem frontier_Ici {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] [no_bot_order α] {a : α} :
@[simp]
theorem frontier_Iic {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] [no_top_order α] {a : α} :
@[simp]
theorem frontier_Ioi {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] [no_top_order α] {a : α} :
@[simp]
theorem frontier_Iio {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] [no_bot_order α] {a : α} :
@[simp]
theorem frontier_Icc {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] [no_bot_order α] [no_top_order α] {a b : α} (h : a < b) :
frontier (set.Icc a b) = {a, b}
@[simp]
theorem frontier_Ioo {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} (h : a < b) :
frontier (set.Ioo a b) = {a, b}
@[simp]
theorem frontier_Ico {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] [no_bot_order α] {a b : α} (h : a < b) :
frontier (set.Ico a b) = {a, b}
@[simp]
theorem frontier_Ioc {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] [no_top_order α] {a b : α} (h : a < b) :
frontier (set.Ioc a b) = {a, b}
theorem nhds_within_Ioi_ne_bot' {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b c : α} (H₁ : a < c) (H₂ : a b) :
theorem nhds_within_Ioi_ne_bot {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] [no_top_order α] {a b : α} (H : a b) :
theorem nhds_within_Ioi_self_ne_bot' {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} (H : a < b) :
@[instance]
theorem nhds_within_Iio_ne_bot' {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b c : α} (H₁ : a < c) (H₂ : b c) :
theorem nhds_within_Iio_ne_bot {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] [no_bot_order α] {a b : α} (H : a b) :
theorem nhds_within_Iio_self_ne_bot' {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} (H : a < b) :
@[instance]
theorem right_nhds_within_Ico_ne_bot {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} (H : a < b) :
theorem left_nhds_within_Ioc_ne_bot {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} (H : a < b) :
theorem left_nhds_within_Ioo_ne_bot {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} (H : a < b) :
theorem right_nhds_within_Ioo_ne_bot {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} (H : a < b) :
theorem comap_coe_nhds_within_Iio_of_Ioo_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {b : α} {s : set α} (hb : s set.Iio b) (hs : s.nonempty(∃ (a : α) (H : a < b), set.Ioo a b s)) :
theorem comap_coe_nhds_within_Ioi_of_Ioo_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a : α} {s : set α} (ha : s set.Ioi a) (hs : s.nonempty(∃ (b : α) (H : b > a), set.Ioo a b s)) :
theorem map_coe_at_top_of_Ioo_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {b : α} {s : set α} (hb : s set.Iio b) (hs : ∀ (a' : α), a' < b(∃ (a : α) (H : a < b), set.Ioo a b s)) :
theorem map_coe_at_bot_of_Ioo_subset {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a : α} {s : set α} (ha : s set.Ioi a) (hs : ∀ (b' : α), b' > a(∃ (b : α) (H : b > a), set.Ioo a b s)) :

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

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

@[simp]
theorem map_coe_Ioo_at_top {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} (h : a < b) :
@[simp]
theorem map_coe_Ioo_at_bot {α : Type u} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} (h : a < b) :
@[simp]
theorem tendsto_comp_coe_Ioo_at_top {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} {l : filter β} {f : α → β} (h : a < b) :
@[simp]
theorem tendsto_comp_coe_Ioo_at_bot {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} {l : filter β} {f : α → β} (h : a < b) :
@[simp]
theorem tendsto_comp_coe_Ioi_at_bot {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a : α} {l : filter β} {f : α → β} :
@[simp]
theorem tendsto_comp_coe_Iio_at_top {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a : α} {l : filter β} {f : α → β} :
@[simp]
theorem tendsto_Ioo_at_top {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} {l : filter β} {f : β → (set.Ioo a b)} :
@[simp]
theorem tendsto_Ioo_at_bot {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a b : α} {l : filter β} {f : β → (set.Ioo a b)} :
@[simp]
theorem tendsto_Ioi_at_bot {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a : α} {l : filter β} {f : β → (set.Ioi a)} :
@[simp]
theorem tendsto_Iio_at_top {α : Type u} {β : Type v} [topological_space α] [linear_order α] [order_topology α] [densely_ordered α] {a : α} {l : filter β} {f : β → (set.Iio a)} :
theorem Sup_mem_closure {α : Type u} [topological_space α] [complete_linear_order α] [order_topology α] {s : set α} (hs : s.nonempty) :
theorem Inf_mem_closure {α : Type u} [topological_space α] [complete_linear_order α] [order_topology α] {s : set α} (hs : s.nonempty) :
theorem is_closed.Sup_mem {α : Type u} [topological_space α] [complete_linear_order α] [order_topology α] {s : set α} (hs : s.nonempty) (hc : is_closed s) :
Sup s s
theorem is_closed.Inf_mem {α : Type u} [topological_space α] [complete_linear_order α] [order_topology α] {s : set α} (hs : s.nonempty) (hc : is_closed s) :
Inf s s
theorem map_Sup_of_continuous_at_of_monotone' {α : Type u} {β : Type v} [complete_linear_order α] [topological_space α] [order_topology α] [complete_linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} (Cf : continuous_at f (Sup s)) (Mf : monotone f) (hs : s.nonempty) :
f (Sup s) = Sup (f '' s)

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

theorem map_Sup_of_continuous_at_of_monotone {α : Type u} {β : Type v} [complete_linear_order α] [topological_space α] [order_topology α] [complete_linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} (Cf : continuous_at f (Sup s)) (Mf : monotone f) (fbot : f = ) :
f (Sup s) = Sup (f '' s)

A monotone function s 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 map_supr_of_continuous_at_of_monotone' {α : Type u} {β : Type v} [complete_linear_order α] [topological_space α] [order_topology α] [complete_linear_order β] [topological_space β] [order_topology β] {ι : Sort u_1} [nonempty ι] {f : α → β} {g : ι → α} (Cf : continuous_at f (supr g)) (Mf : monotone f) :
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 map_supr_of_continuous_at_of_monotone {α : Type u} {β : Type v} [complete_linear_order α] [topological_space α] [order_topology α] [complete_linear_order β] [topological_space β] [order_topology β] {ι : Sort u_1} {f : α → β} {g : ι → α} (Cf : continuous_at f (supr 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 map_Inf_of_continuous_at_of_monotone' {α : Type u} {β : Type v} [complete_linear_order α] [topological_space α] [order_topology α] [complete_linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} (Cf : continuous_at f (Inf s)) (Mf : monotone f) (hs : s.nonempty) :
f (Inf s) = Inf (f '' s)

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

theorem map_Inf_of_continuous_at_of_monotone {α : Type u} {β : Type v} [complete_linear_order α] [topological_space α] [order_topology α] [complete_linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} (Cf : continuous_at f (Inf s)) (Mf : monotone f) (ftop : f = ) :
f (Inf s) = Inf (f '' s)

A monotone function s 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 map_infi_of_continuous_at_of_monotone' {α : Type u} {β : Type v} [complete_linear_order α] [topological_space α] [order_topology α] [complete_linear_order β] [topological_space β] [order_topology β] {ι : Sort u_1} [nonempty ι] {f : α → β} {g : ι → α} (Cf : continuous_at f (infi g)) (Mf : monotone f) :
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 map_infi_of_continuous_at_of_monotone {α : Type u} {β : Type v} [complete_linear_order α] [topological_space α] [order_topology α] [complete_linear_order β] [topological_space β] [order_topology β] {ι : Sort u_1} {f : α → β} {g : ι → α} (Cf : continuous_at f (infi g)) (Mf : monotone f) (ftop : f = ) :
f (infi g) = infi (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 cSup_mem_closure {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : s.nonempty) (B : bdd_above s) :
theorem cInf_mem_closure {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : s.nonempty) (B : bdd_below s) :
theorem is_closed.cSup_mem {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hc : is_closed s) (hs : s.nonempty) (B : bdd_above s) :
Sup s s
theorem is_closed.cInf_mem {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hc : is_closed s) (hs : s.nonempty) (B : bdd_below s) :
Inf s s
theorem map_cSup_of_continuous_at_of_monotone {α : Type u} {β : Type v} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} (Cf : continuous_at f (Sup s)) (Mf : monotone f) (ne : s.nonempty) (H : bdd_above s) :
f (Sup s) = Sup (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 map_csupr_of_continuous_at_of_monotone {α : Type u} {β : Type v} {γ : Type w} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] [nonempty γ] {f : α → β} {g : γ → α} (Cf : continuous_at f (⨆ (i : γ), g i)) (Mf : monotone f) (H : bdd_above (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 map_cInf_of_continuous_at_of_monotone {α : Type u} {β : Type v} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} (Cf : continuous_at f (Inf s)) (Mf : monotone f) (ne : s.nonempty) (H : bdd_below s) :
f (Inf s) = Inf (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 map_cinfi_of_continuous_at_of_monotone {α : Type u} {β : Type v} {γ : Type w} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] [nonempty γ] {f : α → β} {g : γ → α} (Cf : continuous_at f (⨅ (i : γ), g i)) (Mf : monotone f) (H : bdd_below (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 is_connected.Ioo_cInf_cSup_subset {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_connected s) (hb : bdd_below s) (ha : bdd_above s) :
set.Ioo (Inf s) (Sup s) s

A bounded connected subset of a conditionally complete linear order includes the open interval (Inf s, Sup s).

theorem is_preconnected.mem_intervals {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_preconnected s) :
s {set.Icc (Inf s) (Sup s), set.Ico (Inf s) (Sup s), set.Ioc (Inf s) (Sup s), set.Ioo (Inf s) (Sup s), set.Ici (Inf s), set.Ioi (Inf s), set.Iic (Sup s), set.Iio (Sup s), set.univ, }

A preconnected set in a conditionally complete linear order is either one of the intervals [Inf s, Sup s], [Inf s, Sup s), (Inf s, Sup s], (Inf s, Sup s), [Inf s, +∞), (Inf s, +∞), (-∞, Sup s], (-∞, Sup s), (-∞, +∞), or . The converse statement requires α to be densely ordererd.

A preconnected set is either one of the intervals Icc, Ico, Ioc, Ioo, Ici, Ioi, Iic, Iio, or univ, or . The converse statement requires α to be densely ordererd. Though one can represent as (Inf s, Inf s), we include it into the list of possible cases to improve readability.

theorem is_closed.mem_of_ge_of_forall_exists_gt {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {a b : α} {s : set α} (hs : is_closed (s set.Icc a b)) (ha : a s) (hab : a b) (hgt : ∀ (x : α), x s set.Ico a b(s set.Ioc x b).nonempty) :
b s

A "continuous induction principle" for a closed interval: if a set s meets [a, b] on a closed subset, contains a, and the set s ∩ [a, b) has no maximal point, then b ∈ s.

theorem is_closed.Icc_subset_of_forall_exists_gt {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {a b : α} {s : set α} (hs : is_closed (s set.Icc a b)) (ha : a s) (hgt : ∀ (x : α), x s set.Ico a b∀ (y : α), y set.Ioi x(s set.Ioc x y).nonempty) :
set.Icc a b s

A "continuous induction principle" for a closed interval: if a set s meets [a, b] on a closed subset, contains a, and for any a ≤ x < y ≤ b, x ∈ s, the set s ∩ (x, y] is not empty, then [a, b] ⊆ s.

theorem is_closed.Icc_subset_of_forall_mem_nhds_within {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {a b : α} {s : set α} (hs : is_closed (s set.Icc a b)) (ha : a s) (hgt : ∀ (x : α), x s set.Ico a bs 𝓝[set.Ioi x] x) :
set.Icc a b s

A "continuous induction principle" for a closed interval: if a set s meets [a, b] on a closed subset, contains a, and for any x ∈ s ∩ [a, b) the set s includes some open neighborhood of x within (x, +∞), then [a, b] ⊆ s.

A closed interval in a densely ordered conditionally complete linear order is preconnected.

In a dense conditionally complete linear order, the set of preconnected sets is exactly the set of the intervals Icc, Ico, Ioc, Ioo, Ici, Ioi, Iic, Iio, (-∞, +∞), or . Though one can represent as (Inf s, Inf s), we include it into the list of possible cases to improve readability.

theorem intermediate_value_Icc {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Icc (f a) (f b) f '' set.Icc a b

Intermediate Value Theorem for continuous functions on closed intervals, case f a ≤ t ≤ f b.

theorem intermediate_value_Icc' {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Icc (f b) (f a) f '' set.Icc a b

Intermediate Value Theorem for continuous functions on closed intervals, case f a ≥ t ≥ f b.

theorem intermediate_value_interval {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} {f : α → δ} (hf : continuous_on f (set.interval a b)) :
set.interval (f a) (f b) f '' set.interval a b

Intermediate Value Theorem for continuous functions on closed intervals, unordered case.

theorem intermediate_value_Ico {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Ico (f a) (f b) f '' set.Ico a b
theorem intermediate_value_Ico' {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Ioc (f b) (f a) f '' set.Ico a b
theorem intermediate_value_Ioc {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Ioc (f a) (f b) f '' set.Ioc a b
theorem intermediate_value_Ioc' {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Ico (f b) (f a) f '' set.Ioc a b
theorem intermediate_value_Ioo {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Ioo (f a) (f b) f '' set.Ioo a b
theorem intermediate_value_Ioo' {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Ioo (f b) (f a) f '' set.Ioo a b

A continuous function which tendsto at_top at_top and to at_bot at_bot is surjective.

A continuous function which tendsto at_bot at_top and to at_top at_bot is surjective.

If a function f : α → β is continuous on a nonempty interval s, its restriction to s tends to at_bot : filter β along at_bot : filter ↥s and tends to at_top : filter β along at_top : filter ↥s, then the restriction of f to s is surjective. We formulate the conclusion as surj_on f s univ.

If a function f : α → β is continuous on a nonempty interval s, its restriction to s tends to at_top : filter β along at_bot : filter ↥s and tends to at_bot : filter β along at_top : filter ↥s, then the restriction of f to s is surjective. We formulate the conclusion as surj_on f s univ.

theorem compact_Icc {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {a b : α} :

A closed interval in a conditionally complete linear order is compact.

An unordered closed interval in a conditionally complete linear order is compact.

theorem compact_pi_Icc {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), conditionally_complete_linear_order (α i)] [Π (i : ι), topological_space (α i)] [∀ (i : ι), order_topology (α i)] (a b : Π (i : ι), α i) :
@[protected, instance]
@[protected, instance]
def compact_space_pi_Icc {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), conditionally_complete_linear_order (α i)] [Π (i : ι), topological_space (α i)] [∀ (i : ι), order_topology (α i)] (a b : Π (i : ι), α i) :
theorem is_compact.Inf_mem {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
Inf s s
theorem is_compact.Sup_mem {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
Sup s s
theorem is_compact.is_glb_Inf {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
is_glb s (Inf s)
theorem is_compact.is_lub_Sup {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
is_lub s (Sup s)
theorem is_compact.is_least_Inf {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
theorem is_compact.exists_is_least {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
∃ (x : α), is_least s x
theorem is_compact.exists_is_greatest {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
∃ (x : α), is_greatest s x
theorem is_compact.exists_is_glb {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
∃ (x : α) (H : x s), is_glb s x
theorem is_compact.exists_is_lub {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
∃ (x : α) (H : x s), is_lub s x
theorem is_compact.exists_Inf_image_eq {β : Type v} [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) {f : α → β} (hf : continuous_on f s) :
∃ (x : α) (H : x s), Inf (f '' s) = f x
theorem is_compact.exists_Sup_image_eq {β : Type v} [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {α : Type u} [topological_space α] {s : set α} :
is_compact ss.nonempty∀ {f : α → β}, continuous_on f s(∃ (x : α) (H : x s), Sup (f '' s) = f x)
theorem eq_Icc_of_connected_compact {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (h₁ : is_connected s) (h₂ : is_compact s) :
s = set.Icc (Inf s) (Sup s)
theorem is_compact.exists_forall_le {β : Type v} [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) {f : α → β} (hf : continuous_on f s) :
∃ (x : α) (H : x s), ∀ (y : α), y sf x f y

The extreme value theorem: a continuous function realizes its minimum on a compact set

theorem is_compact.exists_forall_ge {β : Type v} [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {α : Type u} [topological_space α] {s : set α} :
is_compact ss.nonempty∀ {f : α → β}, continuous_on f s(∃ (x : α) (H : x s), ∀ (y : α), y sf y f x)

The extreme value theorem: a continuous function realizes its maximum on a compact set

theorem continuous.exists_forall_le {β : Type v} [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {α : Type u_1} [topological_space α] [nonempty α] {f : α → β} (hf : continuous f) (hlim : filter.tendsto f (filter.cocompact α) filter.at_top) :
∃ (x : α), ∀ (y : α), f x f y

The extreme value theorem: if a continuous function f tends to infinity away from compact sets, then it has a global minimum.

theorem continuous.exists_forall_ge {β : Type v} [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {α : Type u_1} [topological_space α] [nonempty α] {f : α → β} (hf : continuous f) (hlim : filter.tendsto f (filter.cocompact α) filter.at_bot) :
∃ (x : α), ∀ (y : α), f y f x

The extreme value theorem: if a continuous function f tends to negative infinity away from compactx sets, then it has a global maximum.

theorem filter.tendsto.is_bounded_under_le {α : Type u} {β : Type v} [semilattice_sup α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} (h : filter.tendsto u f (𝓝 a)) :
theorem filter.tendsto.is_cobounded_under_ge {α : Type u} {β : Type v} [semilattice_sup α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} [f.ne_bot] (h : filter.tendsto u f (𝓝 a)) :
theorem is_bounded_ge_nhds {α : Type u} [semilattice_inf α] [topological_space α] [order_topology α] (a : α) :
theorem filter.tendsto.is_bounded_under_ge {α : Type u} {β : Type v} [semilattice_inf α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} (h : filter.tendsto u f (𝓝 a)) :
theorem filter.tendsto.is_cobounded_under_le {α : Type u} {β : Type v} [semilattice_inf α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} [f.ne_bot] (h : filter.tendsto u f (𝓝 a)) :
theorem lt_mem_sets_of_Limsup_lt {α : Type u} [conditionally_complete_linear_order α] {f : filter α} {b : α} (h : filter.is_bounded has_le.le f) (l : f.Limsup < b) :
∀ᶠ (a : α) in f, a < b
theorem gt_mem_sets_of_Liminf_gt {α : Type u} [conditionally_complete_linear_order α] {f : filter α} {b : α} :
filter.is_bounded ge fb < f.Liminf(∀ᶠ (a : α) in f, b < a)
theorem le_nhds_of_Limsup_eq_Liminf {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {f : filter α} {a : α} (hl : filter.is_bounded has_le.le f) (hg : filter.is_bounded ge f) (hs : f.Limsup = a) (hi : f.Liminf = a) :
f 𝓝 a

If the liminf and the limsup of a filter coincide, then this filter converges to their common value, at least if the filter is eventually bounded above and below.

theorem Limsup_nhds {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] (a : α) :
(𝓝 a).Limsup = a
theorem Liminf_nhds {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] (a : α) :
(𝓝 a).Liminf = a
theorem Liminf_eq_of_le_nhds {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {f : filter α} {a : α} [f.ne_bot] (h : f 𝓝 a) :
f.Liminf = a

If a filter is converging, its limsup coincides with its limit.

theorem Limsup_eq_of_le_nhds {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {f : filter α} {a : α} [f.ne_bot] :
f 𝓝 af.Limsup = a

If a filter is converging, its liminf coincides with its limit.

theorem filter.tendsto.limsup_eq {α : Type u} {β : Type v} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} [f.ne_bot] (h : filter.tendsto u f (𝓝 a)) :
f.limsup u = a

If a function has a limit, then its limsup coincides with its limit.

theorem filter.tendsto.liminf_eq {α : Type u} {β : Type v} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} [f.ne_bot] (h : filter.tendsto u f (𝓝 a)) :
f.liminf u = a

If a function has a limit, then its liminf coincides with its limit.

theorem tendsto_of_liminf_eq_limsup {α : Type u} {β : Type v} [complete_linear_order α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} (hinf : f.liminf u = a) (hsup : f.limsup u = a) :

If the liminf and the limsup of a function coincide, then the limit of the function exists and has the same value

theorem tendsto_of_le_liminf_of_limsup_le {α : Type u} {β : Type v} [complete_linear_order α] [topological_space α] [order_topology α] {f : filter β} {u : β → α} {a : α} (hinf : a f.liminf u) (hsup : f.limsup u a) :

If a number a is less than or equal to the liminf of a function f at some filter and is greater than or equal to the limsup of f, then f tends to a along this filter.

Here is a counter-example to a version of the following with conditionally_complete_lattice α. Take α = [0, 1) → ℝ with the natural lattice structure, ι = ℕ. Put f n x = -x^n. Then ⨆ n, f n = 0 while none of f n is strictly greater than the constant function -0.5.

theorem tendsto_at_top_csupr {ι : Type u_1} {α : Type u_2} [preorder ι] [topological_space α] [conditionally_complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : monotone f) (hbdd : bdd_above (set.range f)) :
filter.tendsto f filter.at_top (𝓝 (⨆ (i : ι), f i))
theorem tendsto_at_bot_cinfi {ι : Type u_1} {α : Type u_2} [preorder ι] [topological_space α] [conditionally_complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : monotone f) (hbdd : bdd_below (set.range f)) :
filter.tendsto f filter.at_bot (𝓝 (⨅ (i : ι), f i))
theorem tendsto_at_top_cinfi {ι : Type u_1} {α : Type u_2} [preorder ι] [topological_space α] [conditionally_complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : ∀ ⦃i j : ι⦄, i jf j f i) (hbdd : bdd_below (set.range f)) :
filter.tendsto f filter.at_top (𝓝 (⨅ (i : ι), f i))
theorem tendsto_at_bot_csupr {ι : Type u_1} {α : Type u_2} [preorder ι] [topological_space α] [conditionally_complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : ∀ ⦃i j : ι⦄, i jf j f i) (hbdd : bdd_above (set.range f)) :
filter.tendsto f filter.at_bot (𝓝 (⨆ (i : ι), f i))
theorem tendsto_at_top_supr {ι : Type u_1} {α : Type u_2} [preorder ι] [topological_space α] [complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : monotone f) :
filter.tendsto f filter.at_top (𝓝 (⨆ (i : ι), f i))
theorem tendsto_at_bot_infi {ι : Type u_1} {α : Type u_2} [preorder ι] [topological_space α] [complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : monotone f) :
filter.tendsto f filter.at_bot (𝓝 (⨅ (i : ι), f i))
theorem tendsto_at_top_infi {ι : Type u_1} {α : Type u_2} [preorder ι] [topological_space α] [complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : ∀ ⦃i j : ι⦄, i jf j f i) :
filter.tendsto f filter.at_top (𝓝 (⨅ (i : ι), f i))
theorem tendsto_at_bot_supr {ι : Type u_1} {α : Type u_2} [preorder ι] [topological_space α] [complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : ∀ ⦃i j : ι⦄, i jf j f i) :
filter.tendsto f filter.at_bot (𝓝 (⨆ (i : ι), f i))
theorem tendsto_of_monotone {ι : Type u_1} {α : Type u_2} [preorder ι] [topological_space α] [conditionally_complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : monotone f) :
theorem supr_eq_of_tendsto {α : Type u_1} {β : Type u_2} [topological_space α] [complete_linear_order α] [order_topology α] [nonempty β] [semilattice_sup β] {f : β → α} {a : α} (hf : monotone f) :
theorem infi_eq_of_tendsto {β : Type v} {α : Type u_1} [topological_space α] [complete_linear_order α] [order_topology α] [nonempty β] [semilattice_sup β] {f : β → α} {a : α} (hf : ∀ (n m : β), n mf m f n) :
theorem nhds_left_sup_nhds_right {α : Type u} (a : α) [topological_space α] [linear_order α] :
theorem nhds_left'_sup_nhds_right {α : Type u} (a : α) [topological_space α] [linear_order α] :
theorem nhds_left_sup_nhds_right' {α : Type u} (a : α) [topological_space α] [linear_order α] :
theorem continuous_at_iff_continuous_left_right {α : Type u} {β : Type v} [topological_space α] [linear_order α] [topological_space β] {a : α} {f : α → β} :
theorem continuous_on_Icc_extend_from_Ioo {α : Type u} {β : Type v} [topological_space α] [linear_order α] [densely_ordered α] [order_topology α] [topological_space β] [regular_space β] {f : α → β} {a b : α} {la lb : β} (hab : a < b) (hf : continuous_on f (set.Ioo a b)) (ha : filter.tendsto f (𝓝[set.Ioi a] a) (𝓝 la)) (hb : filter.tendsto f (𝓝[set.Iio b] b) (𝓝 lb)) :
theorem eq_lim_at_left_extend_from_Ioo {α : Type u} {β : Type v} [topological_space α] [linear_order α] [densely_ordered α] [order_topology α] [topological_space β] [t2_space β] {f : α → β} {a b : α} {la : β} (hab : a < b) (ha : filter.tendsto f (𝓝[set.Ioi a] a) (𝓝 la)) :
extend_from (set.Ioo a b) f a = la
theorem eq_lim_at_right_extend_from_Ioo {α : Type u} {β : Type v} [topological_space α] [linear_order α] [densely_ordered α] [order_topology α] [topological_space β] [t2_space β] {f : α → β} {a b : α} {lb : β} (hab : a < b) (hb : filter.tendsto f (𝓝[set.Iio b] b) (𝓝 lb)) :
extend_from (set.Ioo a b) f b = lb
theorem continuous_on_Ico_extend_from_Ioo {α : Type u} {β : Type v} [topological_space α] [linear_order α] [densely_ordered α] [order_topology α] [topological_space β] [regular_space β] {f : α → β} {a b : α} {la : β} (hab : a < b) (hf : continuous_on f (set.Ioo a b)) (ha : filter.tendsto f (𝓝[set.Ioi a] a) (𝓝 la)) :
theorem continuous_on_Ioc_extend_from_Ioo {α : Type u} {β : Type v} [topological_space α] [linear_order α] [densely_ordered α] [order_topology α] [topological_space β] [regular_space β] {f : α → β} {a b : α} {lb : β} (hab : a < b) (hf : continuous_on f (set.Ioo a b)) (hb : filter.tendsto f (𝓝[set.Iio b] b) (𝓝 lb)) :
theorem continuous_within_at_Ioi_iff_Ici {α : Type u_1} {β : Type u_2} [topological_space α] [partial_order α] [topological_space β] {a : α} {f : α → β} :
theorem continuous_within_at_Iio_iff_Iic {α : Type u_1} {β : Type u_2} [topological_space α] [linear_order α] [topological_space β] {a : α} {f : α → β} :
theorem continuous_at_iff_continuous_left'_right' {α : Type u} {β : Type v} [topological_space α] [linear_order α] [topological_space β] {a : α} {f : α → β} :

Continuity of monotone functions #

In this section we prove the following fact: if f is a monotone function on a neighborhood of a and the image of this neighborhood is a neighborhood of f a, then f is continuous at a, see continuous_at_of_mono_incr_on_of_image_mem_nhds, as well as several similar facts.

theorem strict_mono_incr_on.continuous_at_right_of_exists_between {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_incr_on f s) (hs : s 𝓝[set.Ici a] a) (hfs : ∀ (b : β), b > f a(∃ (c : α) (H : c s), f c set.Ioc (f a) b)) :

If f is a function strictly monotonically increasing on a right neighborhood of a and the image of this neighborhood under f meets every interval (f a, b], b > f a, then f is continuous at a from the right.

The assumption hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b is required because otherwise the function f : ℝ → ℝ given by f x = if x ≤ 0 then x else x + 1 would be a counter-example at a = 0.

theorem continuous_at_right_of_mono_incr_on_of_exists_between {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : ∀ (x : α), x s∀ (y : α), y sx yf x f y) (hs : s 𝓝[set.Ici a] a) (hfs : ∀ (b : β), b > f a(∃ (c : α) (H : c s), f c set.Ioo (f a) b)) :

If f is a function monotonically increasing function on a right neighborhood of a and the image of this neighborhood under f meets every interval (f a, b), b > f a, then f is continuous at a from the right.

The assumption hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b cannot be replaced by the weaker assumption hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b we use for strictly monotone functions because otherwise the function ceil : ℝ → ℤ would be a counter-example at a = 0.

theorem continuous_at_right_of_mono_incr_on_of_closure_image_mem_nhds_within {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : ∀ (x : α), x s∀ (y : α), y sx yf x f y) (hs : s 𝓝[set.Ici a] a) (hfs : closure (f '' s) 𝓝[set.Ici (f a)] f a) :

If a function f with a densely ordered codomain is monotonically increasing on a right neighborhood of a and the closure of the image of this neighborhood under f is a right neighborhood of f a, then f is continuous at a from the right.

theorem continuous_at_right_of_mono_incr_on_of_image_mem_nhds_within {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : ∀ (x : α), x s∀ (y : α), y sx yf x f y) (hs : s 𝓝[set.Ici a] a) (hfs : f '' s 𝓝[set.Ici (f a)] f a) :

If a function f with a densely ordered codomain is monotonically increasing on a right neighborhood of a and the image of this neighborhood under f is a right neighborhood of f a, then f is continuous at a from the right.

theorem strict_mono_incr_on.continuous_at_right_of_closure_image_mem_nhds_within {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_incr_on f s) (hs : s 𝓝[set.Ici a] a) (hfs : closure (f '' s) 𝓝[set.Ici (f a)] f a) :

If a function f with a densely ordered codomain is strictly monotonically increasing on a right neighborhood of a and the closure of the image of this neighborhood under f is a right neighborhood of f a, then f is continuous at a from the right.

theorem strict_mono_incr_on.continuous_at_right_of_image_mem_nhds_within {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_incr_on f s) (hs : s 𝓝[set.Ici a] a) (hfs : f '' s 𝓝[set.Ici (f a)] f a) :

If a function f with a densely ordered codomain is strictly monotonically increasing on a right neighborhood of a and the image of this neighborhood under f is a right neighborhood of f a, then f is continuous at a from the right.

theorem strict_mono_incr_on.continuous_at_right_of_surj_on {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_incr_on f s) (hs : s 𝓝[set.Ici a] a) (hfs : set.surj_on f s (set.Ioi (f a))) :

If a function f is strictly monotonically increasing on a right neighborhood of a and the image of this neighborhood under f includes Ioi (f a), then f is continuous at a from the right.

theorem strict_mono_incr_on.continuous_at_left_of_exists_between {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_incr_on f s) (hs : s 𝓝[set.Iic a] a) (hfs : ∀ (b : β), b < f a(∃ (c : α) (H : c s), f c set.Ico b (f a))) :

If f is a function strictly monotonically increasing on a left neighborhood of a and the image of this neighborhood under f meets every interval [b, f a), b < f a, then f is continuous at a from the left.

The assumption hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a) is required because otherwise the function f : ℝ → ℝ given by f x = if x < 0 then x else x + 1 would be a counter-example at a = 0.

theorem continuous_at_left_of_mono_incr_on_of_exists_between {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : ∀ (x : α), x s∀ (y : α), y sx yf x f y) (hs : s 𝓝[set.Iic a] a) (hfs : ∀ (b : β), b < f a(∃ (c : α) (H : c s), f c set.Ioo b (f a))) :

If f is a function monotonically increasing function on a left neighborhood of a and the image of this neighborhood under f meets every interval (b, f a), b < f a, then f is continuous at a from the left.

The assumption hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ioo b (f a) cannot be replaced by the weaker assumption hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a) we use for strictly monotone functions because otherwise the function floor : ℝ → ℤ would be a counter-example at a = 0.

theorem continuous_at_left_of_mono_incr_on_of_closure_image_mem_nhds_within {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : ∀ (x : α), x s∀ (y : α), y sx yf x f y) (hs : s 𝓝[set.Iic a] a) (hfs : closure (f '' s) 𝓝[set.Iic (f a)] f a) :

If a function f with a densely ordered codomain is monotonically increasing on a left neighborhood of a and the closure of the image of this neighborhood under f is a left neighborhood of f a, then f is continuous at a from the left

theorem continuous_at_left_of_mono_incr_on_of_image_mem_nhds_within {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : ∀ (x : α), x s∀ (y : α), y sx yf x f y) (hs : s 𝓝[set.Iic a] a) (hfs : f '' s 𝓝[set.Iic (f a)] f a) :

If a function f with a densely ordered codomain is monotonically increasing on a left neighborhood of a and the image of this neighborhood under f is a left neighborhood of f a, then f is continuous at a from the left.

theorem strict_mono_incr_on.continuous_at_left_of_closure_image_mem_nhds_within {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_incr_on f s) (hs : s 𝓝[set.Iic a] a) (hfs : closure (f '' s) 𝓝[set.Iic (f a)] f a) :

If a function f with a densely ordered codomain is strictly monotonically increasing on a left neighborhood of a and the closure of the image of this neighborhood under f is a left neighborhood of f a, then f is continuous at a from the left.

theorem strict_mono_incr_on.continuous_at_left_of_image_mem_nhds_within {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_incr_on f s) (hs : s 𝓝[set.Iic a] a) (hfs : f '' s 𝓝[set.Iic (f a)] f a) :

If a function f with a densely ordered codomain is strictly monotonically increasing on a left neighborhood of a and the image of this neighborhood under f is a left neighborhood of f a, then f is continuous at a from the left.

theorem strict_mono_incr_on.continuous_at_left_of_surj_on {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_incr_on f s) (hs : s 𝓝[set.Iic a] a) (hfs : set.surj_on f s (set.Iio (f a))) :

If a function f is strictly monotonically increasing on a left neighborhood of a and the image of this neighborhood under f includes Iio (f a), then f is continuous at a from the left.

theorem strict_mono_incr_on.continuous_at_of_exists_between {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_incr_on f s) (hs : s 𝓝 a) (hfs_l : ∀ (b : β), b < f a(∃ (c : α) (H : c s), f c set.Ico b (f a))) (hfs_r : ∀ (b : β), b > f a(∃ (c : α) (H : c s), f c set.Ioc (f a) b)) :

If a function f is strictly monotonically increasing on a neighborhood of a and the image of this neighborhood under f meets every interval [b, f a), b < f a, and every interval (f a, b], b > f a, then f is continuous at a.

theorem strict_mono_incr_on.continuous_at_of_closure_image_mem_nhds {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_incr_on f s) (hs : s 𝓝 a) (hfs : closure (f '' s) 𝓝 (f a)) :

If a function f with a densely ordered codomain is strictly monotonically increasing on a neighborhood of a and the closure of the image of this neighborhood under f is a neighborhood of f a, then f is continuous at a.

theorem strict_mono_incr_on.continuous_at_of_image_mem_nhds {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_incr_on f s) (hs : s 𝓝 a) (hfs : f '' s 𝓝 (f a)) :

If a function f with a densely ordered codomain is strictly monotonically increasing on a neighborhood of a and the image of this set under f is a neighborhood of f a, then f is continuous at a.

theorem continuous_at_of_mono_incr_on_of_exists_between {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : ∀ (x : α), x s∀ (y : α), y sx yf x f y) (hs : s 𝓝 a) (hfs_l : ∀ (b : β), b < f a(∃ (c : α) (H : c s), f c set.Ioo b (f a))) (hfs_r : ∀ (b : β), b > f a(∃ (c : α) (H : c s), f c set.Ioo (f a) b)) :

If f is a function monotonically increasing function on a neighborhood of a and the image of this neighborhood under f meets every interval (b, f a), b < f a, and every interval (f a, b), b > f a, then f is continuous at a.

theorem continuous_at_of_mono_incr_on_of_closure_image_mem_nhds {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : ∀ (x : α), x s∀ (y : α), y sx yf x f y) (hs : s 𝓝 a) (hfs : closure (f '' s) 𝓝 (f a)) :

If a function f with a densely ordered codomain is monotonically increasing on a neighborhood of a and the closure of the image of this neighborhood under f is a neighborhood of f a, then f is continuous at a.

theorem continuous_at_of_mono_incr_on_of_image_mem_nhds {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : ∀ (x : α), x s∀ (y : α), y sx yf x f y) (hs : s 𝓝 a) (hfs : f '' s 𝓝 (f a)) :

If a function f with a densely ordered codomain is monotonically increasing on a neighborhood of a and the image of this neighborhood under f is a neighborhood of f a, then f is continuous at a.

theorem monotone.continuous_of_dense_range {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} (h_mono : monotone f) (h_dense : dense_range f) :

A monotone function with densely ordered codomain and a dense range is continuous.

theorem monotone.continuous_of_surjective {α : Type u} {β : Type v} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} (h_mono : monotone f) (h_surj : function.surjective f) :

A monotone surjective function with a densely ordered codomain is surjective.

Continuity of order isomorphisms #

In this section we prove that an order_iso is continuous, hence it is a homeomorph. We prove this for an order_iso between to partial orders with order topology.

@[protected]
theorem order_iso.continuous {α : Type u} {β : Type v} [partial_order α] [partial_order β] [topological_space α] [topological_space β] [order_topology α] [order_topology β] (e : α ≃o β) :
def order_iso.to_homeomorph {α : Type u} {β : Type v} [partial_order α] [partial_order β] [topological_space α] [topological_space β] [order_topology α] [order_topology β] (e : α ≃o β) :
α ≃ₜ β

An order isomorphism between two linear order order_topology spaces is a homeomorphism.

Equations
@[simp]
theorem order_iso.coe_to_homeomorph {α : Type u} {β : Type v} [partial_order α] [partial_order β] [topological_space α] [topological_space β] [order_topology α] [order_topology β] (e : α ≃o β) :
@[simp]
theorem order_iso.coe_to_homeomorph_symm {α : Type u} {β : Type v} [partial_order α] [partial_order β] [topological_space α] [topological_space β] [order_topology α] [order_topology β] (e : α ≃o β) :