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
is_open_lt: iffandgare continuous functions, then{x | f x < g x}is open;is_open_Iio,is_open_Ioi,is_open_Ioo: open intervals are open;is_closed_le: iffandgare continuous functions, then{x | f x ≤ g x}is closed;is_closed_Iic,is_closed_Ici,is_closed_Icc: closed intervals are closed;frontier_le_subset_eq,frontier_lt_subset_eq: frontiers of both{x | f x ≤ g x}and{x | f x < g x}are included by{x | f x = g x};exists_Ioc_subset_of_mem_nhds,exists_Ico_subset_of_mem_nhds: ifx < y, then any neighborhood ofxincludes an interval[x, z)for somez ∈ (x, y], and any neighborhood ofyincludes an interval(z, y]for somez ∈ [x, y).
Convergence and inequalities
le_of_tendsto_of_tendsto: iffconverges toa,gconverges tob, and eventuallyf x ≤ g x, thena ≤ ble_of_tendsto,ge_of_tendsto: iffconverges toaand eventuallyf x ≤ b(resp.,b ≤ f x), thena ≤ b(resp.,b ≤ a); we also provide primed versions that assume the inequalities to hold for allx`.
Min, max, Sup and Inf
continuous.min,continuous.max: pointwisemin/maxof two continuous functions is continuous.tendsto.min,tendsto.max: ifftends toaandgtends tob, then their pointwisemin/maxtend tomin a bandmax a b, respectively.tendsto_of_tendsto_of_tendsto_of_le_of_le: theorem known as squeeze theorem, sandwich theorem, theorem of Carabinieri, and two policemen (and a drunk) theorem; ifgandhboth converge toa, and eventuallyg x ≤ f x ≤ h x, thenfconverges toa.
Connected sets and Intermediate Value Theorem
is_preconnected_I??: all intervalsI??are preconnected,is_preconnected.intermediate_value,intermediate_value_univ: Intermediate Value Theorem for connected sets and connected spaces, respectively;intermediate_value_Icc,intermediate_value_Icc': Intermediate Value Theorem for functions on closed intervals.
Miscellaneous facts
is_compact.exists_forall_le,is_compact.exists_forall_ge: extreme value theorem, a continuous function on a compact set takes its minimum and maximum values.is_closed.Icc_subset_of_forall_mem_nhds_within: “Continuous induction” principle; ifs ∩ [a, b]is closed,a ∈ s, and for eachx ∈ [a, b) ∩ ssome of its right neighborhoods is includeds, then[a, b] ⊆ s.is_closed.Icc_subset_of_forall_exists_gt,is_closed.mem_of_ge_of_forall_exists_gt: two other versions of the “continuous induction” principle.
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]
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.
theorem
is_closed_le
{α : Type u}
{β : Type v}
[topological_space α]
[preorder α]
[t : order_closed_topology α]
[topological_space β]
{f g : β → α} :
continuous f → continuous g → is_closed {b : β | f b ≤ g b}
theorem
is_closed_le'
{α : Type u}
[topological_space α]
[preorder α]
[t : order_closed_topology α]
(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 : α) :
theorem
is_closed_Ici
{α : Type u}
[topological_space α]
[preorder α]
[t : order_closed_topology α]
{a : α} :
@[instance]
def
order_dual.order_closed_topology
{α : Type u}
[topological_space α]
[preorder α]
[t : order_closed_topology α] :
Equations
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] :
filter.tendsto f b (nhds a₁) → filter.tendsto g b (nhds a₂) → 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] :
filter.tendsto f b (nhds a₁) → filter.tendsto g b (nhds a₂) → (∀ (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] :
filter.tendsto f x (nhds a) → (∀ᶠ (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] :
filter.tendsto f x (nhds a) → (∀ (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] :
filter.tendsto f x (nhds a) → (∀ᶠ (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] :
filter.tendsto f x (nhds a) → (∀ (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 : β → α} :
continuous f → 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 : β → α} :
continuous f → 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 : β} :
x ∈ closure s → continuous_within_at f s x → continuous_within_at g s x → (∀ (y : β), y ∈ s → f 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 β} :
is_closed s → continuous_on f s → 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 : α} :
a ≤ b → nhds_within b (set.Ici a) ≠ ⊥
theorem
nhds_within_Ici_self_ne_bot
{α : Type u}
[topological_space α]
[preorder α]
(a : α) :
nhds_within a (set.Ici a) ≠ ⊥
theorem
nhds_within_Iic_ne_bot
{α : Type u}
[topological_space α]
[preorder α]
{a b : α} :
a ≤ b → nhds_within a (set.Iic b) ≠ ⊥
theorem
nhds_within_Iic_self_ne_bot
{α : Type u}
[topological_space α]
[preorder α]
(a : α) :
nhds_within a (set.Iic a) ≠ ⊥
@[instance]
def
order_closed_topology.to_t2_space
{α : Type u}
[topological_space α]
[partial_order α]
[t : order_closed_topology α] :
t2_space α
Equations
- order_closed_topology.to_t2_space = _
- _ = _
- _ = _
theorem
is_open_lt
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[topological_space β]
{f g : β → α} :
continuous f → 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
intermediate_value_univ₂
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{γ : Type u_1}
[topological_space γ]
[preconnected_space γ]
{a b : γ}
{f g : γ → α} :
continuous f → continuous g → f a ≤ g a → 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
is_preconnected.intermediate_value₂
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{γ : Type u_1}
[topological_space γ]
{s : set γ}
(hs : is_preconnected s)
{a b : γ}
(ha : a ∈ s)
(hb : b ∈ s)
{f g : γ → α} :
continuous_on f s → continuous_on g s → f a ≤ g a → 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
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{γ : Type u_1}
[topological_space γ]
{s : set γ}
(hs : is_preconnected s)
{a b : γ}
(ha : a ∈ s)
(hb : b ∈ s)
{f : γ → α} :
continuous_on f s → set.Icc (f a) (f b) ⊆ f '' s
Intermediate Value Theorem for continuous functions on connected sets.
theorem
intermediate_value_univ
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{γ : Type u_1}
[topological_space γ]
[preconnected_space γ]
(a b : γ)
{f : γ → α} :
continuous f → set.Icc (f a) (f b) ⊆ set.range f
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 : α} :
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 : α} :
If a preconnected set contains endpoints of an interval, then it includes the whole interval.
theorem
is_preconnected.eq_univ_of_unbounded
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{s : set α} :
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 : α} :
theorem
Ioc_mem_nhds_within_Ioi
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
theorem
Ico_mem_nhds_within_Ioi
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
theorem
Icc_mem_nhds_within_Ioi
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
@[simp]
theorem
nhds_within_Ioc_eq_nhds_within_Ioi
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
a < b → nhds_within a (set.Ioc a b) = nhds_within a (set.Ioi a)
@[simp]
theorem
nhds_within_Ioo_eq_nhds_within_Ioi
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
a < b → nhds_within a (set.Ioo a b) = nhds_within a (set.Ioi a)
@[simp]
theorem
continuous_within_at_Ioc_iff_Ioi
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[topological_space β]
{a b : α}
{f : α → β} :
a < b → (continuous_within_at f (set.Ioc a b) a ↔ continuous_within_at f (set.Ioi a) a)
@[simp]
theorem
continuous_within_at_Ioo_iff_Ioi
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[topological_space β]
{a b : α}
{f : α → β} :
a < b → (continuous_within_at f (set.Ioo a b) a ↔ continuous_within_at f (set.Ioi a) a)
Left neighborhoods, point excluded
theorem
Ioo_mem_nhds_within_Iio
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
theorem
Ico_mem_nhds_within_Iio
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
theorem
Ioc_mem_nhds_within_Iio
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
theorem
Icc_mem_nhds_within_Iio
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
@[simp]
theorem
nhds_within_Ico_eq_nhds_within_Iio
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
a < b → nhds_within b (set.Ico a b) = nhds_within b (set.Iio b)
@[simp]
theorem
nhds_within_Ioo_eq_nhds_within_Iio
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
a < b → nhds_within b (set.Ioo a b) = nhds_within b (set.Iio b)
@[simp]
theorem
continuous_within_at_Ico_iff_Iio
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[topological_space β]
{a b : α}
{f : α → β} :
a < b → (continuous_within_at f (set.Ico a b) b ↔ continuous_within_at f (set.Iio b) b)
@[simp]
theorem
continuous_within_at_Ioo_iff_Iio
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[topological_space β]
{a b : α}
{f : α → β} :
a < b → (continuous_within_at f (set.Ioo a b) b ↔ continuous_within_at f (set.Iio b) b)
Right neighborhoods, point included
theorem
Ioo_mem_nhds_within_Ici
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
theorem
Ioc_mem_nhds_within_Ici
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
theorem
Ico_mem_nhds_within_Ici
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
theorem
Icc_mem_nhds_within_Ici
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
@[simp]
theorem
nhds_within_Icc_eq_nhds_within_Ici
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
a < b → nhds_within a (set.Icc a b) = nhds_within a (set.Ici a)
@[simp]
theorem
nhds_within_Ico_eq_nhds_within_Ici
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
a < b → nhds_within a (set.Ico a b) = nhds_within a (set.Ici a)
@[simp]
theorem
continuous_within_at_Icc_iff_Ici
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[topological_space β]
{a b : α}
{f : α → β} :
a < b → (continuous_within_at f (set.Icc a b) a ↔ continuous_within_at f (set.Ici a) a)
@[simp]
theorem
continuous_within_at_Ico_iff_Ici
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[topological_space β]
{a b : α}
{f : α → β} :
a < b → (continuous_within_at f (set.Ico a b) a ↔ continuous_within_at f (set.Ici a) a)
Left neighborhoods, point included
theorem
Ioo_mem_nhds_within_Iic
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
theorem
Ico_mem_nhds_within_Iic
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
theorem
Ioc_mem_nhds_within_Iic
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
theorem
Icc_mem_nhds_within_Iic
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α} :
@[simp]
theorem
nhds_within_Icc_eq_nhds_within_Iic
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
a < b → nhds_within b (set.Icc a b) = nhds_within b (set.Iic b)
@[simp]
theorem
nhds_within_Ioc_eq_nhds_within_Iic
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
a < b → nhds_within b (set.Ioc a b) = nhds_within b (set.Iic 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 : α → β} :
a < b → (continuous_within_at f (set.Icc a b) b ↔ continuous_within_at f (set.Iic b) 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 : α → β} :
a < b → (continuous_within_at f (set.Ioc a b) b ↔ continuous_within_at f (set.Iic b) b)
theorem
frontier_le_subset_eq
{α : Type u}
{β : Type v}
[topological_space α]
[decidable_linear_order α]
[order_closed_topology α]
{f g : β → α}
[topological_space β] :
continuous f → continuous g → frontier {b : β | f b ≤ g b} ⊆ {b : β | f b = g b}
theorem
frontier_lt_subset_eq
{α : Type u}
{β : Type v}
[topological_space α]
[decidable_linear_order α]
[order_closed_topology α]
{f g : β → α}
[topological_space β] :
continuous f → continuous g → frontier {b : β | f b < g b} ⊆ {b : β | f b = g b}
theorem
continuous.min
{α : Type u}
{β : Type v}
[topological_space α]
[decidable_linear_order α]
[order_closed_topology α]
{f g : β → α}
[topological_space β] :
continuous f → continuous g → continuous (λ (b : β), min (f b) (g b))
theorem
continuous.max
{α : Type u}
{β : Type v}
[topological_space α]
[decidable_linear_order α]
[order_closed_topology α]
{f g : β → α}
[topological_space β] :
continuous f → continuous g → continuous (λ (b : β), max (f b) (g b))
theorem
tendsto.max
{α : Type u}
{β : Type v}
[topological_space α]
[decidable_linear_order α]
[order_closed_topology α]
{f g : β → α}
{b : filter β}
{a₁ a₂ : α} :
filter.tendsto f b (nhds a₁) → filter.tendsto g b (nhds a₂) → filter.tendsto (λ (b : β), max (f b) (g b)) b (nhds (max a₁ a₂))
theorem
tendsto.min
{α : Type u}
{β : Type v}
[topological_space α]
[decidable_linear_order α]
[order_closed_topology α]
{f g : β → α}
{b : filter β}
{a₁ a₂ : α} :
filter.tendsto f b (nhds a₁) → filter.tendsto g b (nhds a₂) → filter.tendsto (λ (b : β), min (f b) (g b)) b (nhds (min a₁ a₂))
@[class]
- topology_eq_generate_intervals : t = topological_space.generate_from {s : set α | ∃ (a : α), s = set.Ioi a ∨ s = set.Iio a}
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.
(Order) topology on a partial order α generated by the subbase of open intervals
(a, ∞) = { x ∣ a < x }, (-∞ , b) = {x ∣ x < b} for all a, b in α. We do not register it as an
instance as many ordered sets are already endowed with the same topology, most often in a non-defeq
way though. Register as a local instance when necessary.
Equations
- preorder.topology α = topological_space.generate_from {s : set α | ∃ (a : α), s = {b : α | a < b} ∨ s = {b : α | b < a}}
@[instance]
def
order_dual.order_topology
{α : Type u_1}
[topological_space α]
[partial_order α]
[order_topology α] :
Equations
theorem
is_open_iff_generate_intervals
{α : Type u}
[topological_space α]
[partial_order α]
[t : order_topology α]
{s : set α} :
theorem
is_open_lt'
{α : Type u}
[topological_space α]
[partial_order α]
[t : order_topology α]
(a : α) :
theorem
is_open_gt'
{α : Type u}
[topological_space α]
[partial_order α]
[t : order_topology α]
(a : α) :
theorem
lt_mem_nhds
{α : Type u}
[topological_space α]
[partial_order α]
[t : order_topology α]
{a b : α} :
theorem
le_mem_nhds
{α : Type u}
[topological_space α]
[partial_order α]
[t : order_topology α]
{a b : α} :
theorem
gt_mem_nhds
{α : Type u}
[topological_space α]
[partial_order α]
[t : order_topology α]
{a b : α} :
theorem
ge_mem_nhds
{α : Type u}
[topological_space α]
[partial_order α]
[t : order_topology α]
{a b : α} :
theorem
nhds_eq_order
{α : Type u}
[topological_space α]
[partial_order α]
[t : order_topology α]
(a : α) :
theorem
tendsto_order
{α : Type u}
{β : Type v}
[topological_space α]
[partial_order α]
[t : order_topology α]
{f : β → α}
{a : α}
{x : filter β} :
@[instance]
def
tendsto_Icc_class_nhds
{α : Type u}
[topological_space α]
[partial_order α]
[t : order_topology α]
(a : α) :
filter.tendsto_Ixx_class set.Icc (nhds a) (nhds a)
Equations
- _ = _
@[instance]
def
tendsto_Ico_class_nhds
{α : Type u}
[topological_space α]
[partial_order α]
[t : order_topology α]
(a : α) :
filter.tendsto_Ixx_class set.Ico (nhds a) (nhds a)
Equations
- _ = _
@[instance]
def
tendsto_Ioc_class_nhds
{α : Type u}
[topological_space α]
[partial_order α]
[t : order_topology α]
(a : α) :
filter.tendsto_Ixx_class set.Ioc (nhds a) (nhds a)
Equations
- _ = _
@[instance]
def
tendsto_Ioo_class_nhds
{α : Type u}
[topological_space α]
[partial_order α]
[t : order_topology α]
(a : α) :
filter.tendsto_Ixx_class set.Ioo (nhds a) (nhds a)
Equations
- _ = _
@[instance]
def
tendsto_Ixx_nhds_within
{α : Type u}
[topological_space α]
[partial_order α]
(a : α)
{s t : set α}
{Ixx : α → α → set α}
[filter.tendsto_Ixx_class Ixx (nhds a) (nhds a)]
[filter.tendsto_Ixx_class Ixx (filter.principal s) (filter.principal t)] :
filter.tendsto_Ixx_class Ixx (nhds_within a s) (nhds_within a t)
Equations
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 : α} :
filter.tendsto g b (nhds a) → filter.tendsto h b (nhds a) → (∀ᶠ (b : β) in b, g b ≤ f b) → (∀ᶠ (b : β) in b, f b ≤ h b) → filter.tendsto f b (nhds a)
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 : α} :
filter.tendsto g b (nhds a) → filter.tendsto h b (nhds a) → g ≤ f → f ≤ h → filter.tendsto f b (nhds a)
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 : α} :
theorem
tendsto_order_unbounded
{α : Type u}
{β : Type v}
[topological_space α]
[partial_order α]
[t : order_topology α]
{f : β → α}
{a : α}
{x : filter β} :
theorem
induced_order_topology'
{α : Type u}
{β : Type v}
[partial_order α]
[ta : topological_space β]
[partial_order β]
[order_topology β]
(f : α → β) :
theorem
induced_order_topology
{α : Type u}
{β : Type v}
[partial_order α]
[ta : topological_space β]
[partial_order β]
[order_topology β]
(f : α → β) :
theorem
exists_Ioc_subset_of_mem_nhds'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α}
(hs : s ∈ nhds a)
{l : α} :
theorem
exists_Ico_subset_of_mem_nhds'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α}
(hs : s ∈ nhds a)
{u : α} :
theorem
exists_Ioc_subset_of_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α} :
theorem
exists_Ico_subset_of_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α} :
theorem
mem_nhds_unbounded
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α} :
theorem
order_separated
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a₁ a₂ : α} :
@[instance]
def
order_topology.to_order_closed_topology
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α] :
Equations
- order_topology.to_order_closed_topology = _
- _ = _
- _ = _
- _ = _
theorem
order_topology.t2_space
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α] :
t2_space α
@[instance]
def
order_topology.regular_space
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α] :
theorem
mem_nhds_iff_exists_Ioo_subset'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a l' u' : α}
{s : set α} :
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 α} :
A set is a neighborhood of a if and only if it contains an interval (l, u) containing a.
theorem
Iio_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a b : α} :
theorem
Ioi_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a b : α} :
theorem
Ioo_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a b x : α} :
theorem
disjoint_nhds_at_top
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[no_top_order α]
(x : α) :
@[simp]
theorem
inf_nhds_at_top
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[no_top_order α]
(x : α) :
nhds x ⊓ filter.at_top = ⊥
theorem
disjoint_nhds_at_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[no_bot_order α]
(x : α) :
@[simp]
theorem
inf_nhds_at_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[no_bot_order α]
(x : α) :
nhds x ⊓ filter.at_bot = ⊥
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 : α) :
¬filter.tendsto f F (nhds 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 : α} :
filter.tendsto f F (nhds x) → ¬filter.tendsto f F filter.at_top
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 : α) :
¬filter.tendsto f F (nhds 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 : α} :
filter.tendsto f F (nhds x) → ¬filter.tendsto f F filter.at_bot
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 α) :
The following statements are equivalent:
sis a neighborhood ofawithin(a, +∞)sis a neighborhood ofawithin(a, b]sis a neighborhood ofawithin(a, b)sincludes(a, u)for someu ∈ (a, b]sincludes(a, u)for someu > a
theorem
mem_nhds_within_Ioi_iff_exists_mem_Ioc_Ioo_subset
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a u' : α}
{s : set α} :
theorem
mem_nhds_within_Ioi_iff_exists_Ioo_subset'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a u' : α}
{s : set α} :
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 α} :
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 α} :
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 α) :
The following statements are equivalent:
sis a neighborhood ofbwithin(-∞, b)sis a neighborhood ofbwithin[a, b)sis a neighborhood ofbwithin(a, b)sincludes(l, b)for somel ∈ [a, b)sincludes(l, b)for somel < b
theorem
mem_nhds_within_Iio_iff_exists_mem_Ico_Ioo_subset
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a l' : α}
{s : set α} :
theorem
mem_nhds_within_Iio_iff_exists_Ioo_subset'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a l' : α}
{s : set α} :
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 α} :
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 α} :
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 α) :
The following statements are equivalent:
sis a neighborhood ofawithin[a, +∞)sis a neighborhood ofawithin[a, b]sis a neighborhood ofawithin[a, b)sincludes[a, u)for someu ∈ (a, b]sincludes[a, u)for someu > a
theorem
mem_nhds_within_Ici_iff_exists_mem_Ioc_Ico_subset
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a u' : α}
{s : set α} :
theorem
mem_nhds_within_Ici_iff_exists_Ico_subset'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a u' : α}
{s : set α} :
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 α} :
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 α} :
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 α) :
The following statements are equivalent:
sis a neighborhood ofbwithin(-∞, b]sis a neighborhood ofbwithin[a, b]sis a neighborhood ofbwithin(a, b]sincludes(l, b]for somel ∈ [a, b)sincludes(l, b]for somel < b
theorem
mem_nhds_within_Iic_iff_exists_mem_Ico_Ioc_subset
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a l' : α}
{s : set α} :
theorem
mem_nhds_within_Iic_iff_exists_Ioc_subset'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a l' : α}
{s : set α} :
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 α} :
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 α} :
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 α} :
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 α} :
A set is a neighborhood of a within (-∞, a] if and only if it contains an interval [l, a]
with l < a.
theorem
tendsto_at_top_add_tendsto_left
{α : Type u}
{β : Type v}
[topological_space α]
[linear_ordered_ring α]
[order_topology α]
{l : filter β}
{f g : β → α}
{C : α} :
filter.tendsto f l (nhds C) → filter.tendsto g l filter.at_top → filter.tendsto (λ (x : β), f x + g x) l filter.at_top
In a linearly ordered ring with the order topology, if f tends to C and g tends to
at_top then f + g tends to at_top.
theorem
tendsto_at_bot_add_tendsto_left
{α : Type u}
{β : Type v}
[topological_space α]
[linear_ordered_ring α]
[order_topology α]
{l : filter β}
{f g : β → α}
{C : α} :
filter.tendsto f l (nhds C) → filter.tendsto g l filter.at_bot → filter.tendsto (λ (x : β), f x + g x) l filter.at_bot
In a linearly ordered ring with the order topology, if f tends to C and g tends to
at_bot then f + g tends to at_bot.
theorem
tendsto_at_top_add_tendsto_right
{α : Type u}
{β : Type v}
[topological_space α]
[linear_ordered_ring α]
[order_topology α]
{l : filter β}
{f g : β → α}
{C : α} :
filter.tendsto f l filter.at_top → filter.tendsto g l (nhds C) → filter.tendsto (λ (x : β), f x + g x) l filter.at_top
In a linearly ordered ring with the order topology, if f tends to at_top and g tends to
C then f + g tends to at_top.
theorem
tendsto_at_bot_add_tendsto_right
{α : Type u}
{β : Type v}
[topological_space α]
[linear_ordered_ring α]
[order_topology α]
{l : filter β}
{f g : β → α}
{C : α} :
filter.tendsto f l filter.at_bot → filter.tendsto g l (nhds C) → filter.tendsto (λ (x : β), f x + g x) l filter.at_bot
In a linearly ordered ring with the order topology, if f tends to at_bot and g tends to
C then f + g tends to at_bot.
theorem
neg_preimage_closure
{α : Type u}
[topological_space α]
[ordered_add_comm_group α]
[topological_add_group α]
{s : set α} :
theorem
is_lub.nhds_within_ne_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α} :
is_lub s a → s.nonempty → (nhds_within a s).ne_bot
theorem
is_glb.nhds_within_ne_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α} :
is_glb s a → s.nonempty → (nhds_within a s).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 ⊓ nhds 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 α} :
theorem
is_lub_of_is_lub_of_tendsto
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[linear_order α]
[linear_order β]
[order_topology α]
[order_topology β]
{f : α → β}
{s : set α}
{a : α}
{b : β} :
theorem
is_glb_of_is_glb_of_tendsto
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[linear_order α]
[linear_order β]
[order_topology α]
[order_topology β]
{f : α → β}
{s : set α}
{a : α}
{b : β} :
theorem
is_glb_of_is_lub_of_tendsto
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[linear_order α]
[linear_order β]
[order_topology α]
[order_topology β]
{f : α → β}
{s : set α}
{a : α}
{b : β} :
theorem
is_lub_of_is_glb_of_tendsto
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[linear_order α]
[linear_order β]
[order_topology α]
[order_topology β]
{f : α → β}
{s : set α}
{a : α}
{b : β} :
theorem
mem_closure_of_is_lub
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α} :
theorem
mem_of_is_lub_of_is_closed
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α} :
theorem
mem_closure_of_is_glb
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α} :
theorem
mem_of_is_glb_of_is_closed
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α} :
theorem
is_compact.bdd_below
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[nonempty α]
{s : set α} :
is_compact s → bdd_below s
A compact set is bounded below
theorem
is_compact.bdd_above
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[nonempty α]
{s : set α} :
is_compact s → bdd_above s
A compact set is bounded above
theorem
closure_Ioi'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{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 : α} :
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 : α} :
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 : α} :
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 : α} :
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 : α} :
@[simp]
theorem
frontier_Ioo
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a b : α} :
@[simp]
theorem
frontier_Ico
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_bot_order α]
{a b : α} :
@[simp]
theorem
frontier_Ioc
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_top_order α]
{a b : α} :
theorem
nhds_within_Ioi_ne_bot'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a b c : α} :
a < c → a ≤ b → (nhds_within b (set.Ioi a)).ne_bot
theorem
nhds_within_Ioi_ne_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_top_order α]
{a b : α} :
a ≤ b → (nhds_within b (set.Ioi a)).ne_bot
theorem
nhds_within_Ioi_self_ne_bot'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a b : α} :
a < b → (nhds_within a (set.Ioi a)).ne_bot
@[instance]
theorem
nhds_within_Ioi_self_ne_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_top_order α]
(a : α) :
(nhds_within a (set.Ioi a)).ne_bot
theorem
nhds_within_Iio_ne_bot'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a b c : α} :
a < c → b ≤ c → (nhds_within b (set.Iio c)).ne_bot
theorem
nhds_within_Iio_ne_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_bot_order α]
{a b : α} :
a ≤ b → (nhds_within a (set.Iio b)).ne_bot
theorem
nhds_within_Iio_self_ne_bot'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a b : α} :
a < b → (nhds_within b (set.Iio b)).ne_bot
@[instance]
theorem
nhds_within_Iio_self_ne_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_bot_order α]
(a : α) :
(nhds_within a (set.Iio a)).ne_bot
theorem
Sup_mem_closure
{α : Type u}
[topological_space α]
[complete_linear_order α]
[order_topology α]
{s : set α} :
s.nonempty → has_Sup.Sup s ∈ closure s
theorem
Inf_mem_closure
{α : Type u}
[topological_space α]
[complete_linear_order α]
[order_topology α]
{s : set α} :
s.nonempty → has_Inf.Inf s ∈ closure s
theorem
is_closed.Sup_mem
{α : Type u}
[topological_space α]
[complete_linear_order α]
[order_topology α]
{s : set α} :
s.nonempty → is_closed s → has_Sup.Sup s ∈ s
theorem
is_closed.Inf_mem
{α : Type u}
[topological_space α]
[complete_linear_order α]
[order_topology α]
{s : set α} :
s.nonempty → is_closed s → has_Inf.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 α} :
continuous_at f (has_Sup.Sup s) → monotone f → s.nonempty → f (has_Sup.Sup s) = has_Sup.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 α} :
continuous_at f (has_Sup.Sup s) → monotone f → f ⊥ = ⊥ → f (has_Sup.Sup s) = has_Sup.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 : ι → α} :
continuous_at f (supr g) → 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 : ι → α} :
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 α} :
continuous_at f (has_Inf.Inf s) → monotone f → s.nonempty → f (has_Inf.Inf s) = has_Inf.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 α} :
continuous_at f (has_Inf.Inf s) → monotone f → f ⊤ = ⊤ → f (has_Inf.Inf s) = has_Inf.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 : ι → α} :
continuous_at f (infi g) → 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 : ι → α} :
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 α} :
s.nonempty → bdd_above s → has_Sup.Sup s ∈ closure s
theorem
cInf_mem_closure
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
s.nonempty → bdd_below s → has_Inf.Inf s ∈ closure s
theorem
is_closed.cSup_mem
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
is_closed s → s.nonempty → bdd_above s → has_Sup.Sup s ∈ s
theorem
is_closed.cInf_mem
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
is_closed s → s.nonempty → bdd_below s → has_Inf.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 α} :
continuous_at f (has_Sup.Sup s) → monotone f → s.nonempty → bdd_above s → f (has_Sup.Sup s) = has_Sup.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 : γ → α} :
continuous_at f (⨆ (i : γ), g i) → monotone f → 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 α} :
continuous_at f (has_Inf.Inf s) → monotone f → s.nonempty → bdd_below s → f (has_Inf.Inf s) = has_Inf.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 : γ → α} :
continuous_at f (⨅ (i : γ), g i) → monotone f → 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 α} :
is_connected s → bdd_below s → bdd_above s → set.Ioo (has_Inf.Inf s) (has_Sup.Sup s) ⊆ s
A bounded connected subset of a conditionally complete linear order includes the open interval
(Inf s, Sup s).
theorem
eq_Icc_cInf_cSup_of_connected_bdd_closed
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
is_connected s → bdd_below s → bdd_above s → is_closed s → s = set.Icc (has_Inf.Inf s) (has_Sup.Sup s)
theorem
is_preconnected.Ioi_cInf_subset
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
is_preconnected s → bdd_below s → ¬bdd_above s → set.Ioi (has_Inf.Inf s) ⊆ s
theorem
is_preconnected.Iio_cSup_subset
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
is_preconnected s → ¬bdd_below s → bdd_above s → set.Iio (has_Sup.Sup s) ⊆ s
theorem
is_preconnected.mem_intervals
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
is_preconnected s → s ∈ {set.Icc (has_Inf.Inf s) (has_Sup.Sup s), set.Ico (has_Inf.Inf s) (has_Sup.Sup s), set.Ioc (has_Inf.Inf s) (has_Sup.Sup s), set.Ioo (has_Inf.Inf s) (has_Sup.Sup s), set.Ici (has_Inf.Inf s), set.Ioi (has_Inf.Inf s), set.Iic (has_Sup.Sup s), set.Iio (has_Sup.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.
theorem
set_of_is_preconnected_subset_of_ordered
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α] :
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 α} :
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 α} :
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 α} :
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.
theorem
is_preconnected_Icc
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[densely_ordered α]
{a b : α} :
is_preconnected (set.Icc a b)
A closed interval in a densely ordered conditionally complete linear order is preconnected.
theorem
is_preconnected_interval
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[densely_ordered α]
{a b : α} :
is_preconnected (set.interval a b)
theorem
is_preconnected_iff_ord_connected
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[densely_ordered α]
{s : set α} :
theorem
is_preconnected_Ici
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[densely_ordered α]
{a : α} :
theorem
is_preconnected_Iic
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[densely_ordered α]
{a : α} :
theorem
is_preconnected_Iio
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[densely_ordered α]
{a : α} :
theorem
is_preconnected_Ioi
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[densely_ordered α]
{a : α} :
theorem
is_preconnected_Ioo
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[densely_ordered α]
{a b : α} :
is_preconnected (set.Ioo a b)
theorem
is_preconnected_Ioc
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[densely_ordered α]
{a b : α} :
is_preconnected (set.Ioc a b)
theorem
is_preconnected_Ico
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[densely_ordered α]
{a b : α} :
is_preconnected (set.Ico a b)
@[instance]
def
ordered_connected_space
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[densely_ordered α] :
Equations
theorem
set_of_is_preconnected_eq_of_ordered
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[densely_ordered α] :
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}
{β : Type v}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
[densely_ordered α]
{a b : α}
(hab : a ≤ b)
{f : α → β} :
Intermediate Value Theorem for continuous functions on closed intervals, case f a ≤ t ≤ f b.
theorem
intermediate_value_Icc'
{α : Type u}
{β : Type v}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
[densely_ordered α]
{a b : α}
(hab : a ≤ b)
{f : α → β} :
Intermediate Value Theorem for continuous functions on closed intervals, case f a ≥ t ≥ f b.
theorem
is_compact.Inf_mem
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
is_compact s → s.nonempty → has_Inf.Inf s ∈ s
theorem
is_compact.Sup_mem
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
is_compact s → s.nonempty → has_Sup.Sup s ∈ s
theorem
is_compact.is_glb_Inf
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
is_compact s → s.nonempty → is_glb s (has_Inf.Inf s)
theorem
is_compact.is_lub_Sup
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
is_compact s → s.nonempty → is_lub s (has_Sup.Sup s)
theorem
is_compact.is_least_Inf
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
is_compact s → s.nonempty → is_least s (has_Inf.Inf s)
theorem
is_compact.is_greatest_Sup
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
is_compact s → s.nonempty → is_greatest s (has_Sup.Sup s)
theorem
is_compact.exists_is_least
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
is_compact 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 α} :
is_compact 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 α} :
is_compact 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 α} :
is_compact 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 : α → β} :
continuous_on f s → (∃ (x : α) (H : x ∈ s), has_Inf.Inf (f '' s) = f x)
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 : α → β} :
continuous_on f s → (∃ (x : α) (H : x ∈ s), ∀ (y : α), y ∈ s → f 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 α}
(a : is_compact s)
(a_1 : s.nonempty)
{f : α → β} :
continuous_on f s → (∃ (x : α) (H : x ∈ s), ∀ (y : α), y ∈ s → f y ≤ f x)
The extreme value theorem: a continuous function realizes its maximum on a compact set
theorem
is_compact.exists_Sup_image_eq
{β : Type v}
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{α : Type u}
[topological_space α]
{s : set α}
(a : is_compact s)
(a_1 : s.nonempty)
{f : α → β} :
continuous_on f s → (∃ (x : α) (H : x ∈ s), has_Sup.Sup (f '' s) = f x)
theorem
eq_Icc_of_connected_compact
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α} :
is_connected s → is_compact s → s = set.Icc (has_Inf.Inf s) (has_Sup.Sup s)
theorem
is_bounded_le_nhds
{α : Type u}
[semilattice_sup α]
[topological_space α]
[order_topology α]
(a : α) :
theorem
filter.tendsto.is_bounded_under_le
{α : Type u}
{β : Type v}
[semilattice_sup α]
[topological_space α]
[order_topology α]
{f : filter β}
{u : β → α}
{a : α} :
filter.tendsto u f (nhds a) → filter.is_bounded_under has_le.le f u
theorem
is_cobounded_ge_nhds
{α : Type u}
[semilattice_sup α]
[topological_space α]
[order_topology α]
(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] :
filter.tendsto u f (nhds a) → filter.is_cobounded_under ge f u
theorem
is_bounded_ge_nhds
{α : Type u}
[semilattice_inf α]
[topological_space α]
[order_topology α]
(a : α) :
filter.is_bounded ge (nhds a)
theorem
filter.tendsto.is_bounded_under_ge
{α : Type u}
{β : Type v}
[semilattice_inf α]
[topological_space α]
[order_topology α]
{f : filter β}
{u : β → α}
{a : α} :
filter.tendsto u f (nhds a) → filter.is_bounded_under ge f u
theorem
is_cobounded_le_nhds
{α : Type u}
[semilattice_inf α]
[topological_space α]
[order_topology α]
(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] :
filter.tendsto u f (nhds a) → filter.is_cobounded_under has_le.le f u
theorem
lt_mem_sets_of_Limsup_lt
{α : Type u}
[conditionally_complete_linear_order α]
{f : filter α}
{b : α} :
filter.is_bounded has_le.le f → 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 f → b < 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 : α} :
filter.is_bounded has_le.le f → filter.is_bounded ge f → f.Limsup = a → f.Liminf = a → f ≤ nhds 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 : α) :
theorem
Liminf_nhds
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
(a : α) :
theorem
Liminf_eq_of_le_nhds
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{f : filter α}
{a : α}
[f.ne_bot] :
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] :
If a filter is converging, 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 : α} :
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 : α} :
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.
theorem
filter.tendsto.limsup_eq
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
{f : filter β}
{u : β → α}
{a : α}
[f.ne_bot] :
filter.tendsto u f (nhds 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}
[complete_linear_order α]
[topological_space α]
[order_topology α]
{f : filter β}
{u : β → α}
{a : α}
[f.ne_bot] :
filter.tendsto u f (nhds a) → f.liminf u = a
If a function has a limit, then its liminf coincides with its limit
theorem
order_topology_of_nhds_abs
{α : Type u_1}
[decidable_linear_ordered_add_comm_group α]
[topological_space α] :
(∀ (a : α), nhds a = ⨅ (r : α) (H : r > 0), filter.principal {b : α | abs (a - b) < r}) → order_topology α
theorem
tendsto_at_top_supr_nat
{α : Type u}
[topological_space α]
[complete_linear_order α]
[order_topology α]
(f : ℕ → α) :
monotone f → filter.tendsto f filter.at_top (nhds (⨆ (i : ℕ), f i))
theorem
tendsto_at_top_infi_nat
{α : Type u}
[topological_space α]
[complete_linear_order α]
[order_topology α]
(f : ℕ → α) :
(∀ {n m : ℕ}, n ≤ m → f m ≤ f n) → filter.tendsto f filter.at_top (nhds (⨅ (i : ℕ), f i))
theorem
supr_eq_of_tendsto
{α : Type u_1}
[topological_space α]
[complete_linear_order α]
[order_topology α]
{f : ℕ → α}
{a : α} :
monotone f → filter.tendsto f filter.at_top (nhds a) → supr f = a
theorem
infi_eq_of_tendsto
{α : Type u_1}
[topological_space α]
[complete_linear_order α]
[order_topology α]
{f : ℕ → α}
{a : α} :
(∀ (n m : ℕ), n ≤ m → f m ≤ f n) → filter.tendsto f filter.at_top (nhds a) → infi f = a
$\lim_{x\to+\infty}|x|=+\infty$
theorem
decidable_linear_ordered_add_comm_group.tendsto_nhds
{α : Type u}
[decidable_linear_ordered_add_comm_group α]
[topological_space α]
[order_topology α]
{β : Type u_1}
(f : β → α)
(x : filter β)
(a : α) :
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 : ι → α} :
monotone f → bdd_above (set.range f) → filter.tendsto f filter.at_top (nhds (⨆ (i : ι), f i))
theorem
tendsto_at_top_supr
{ι : Type u_1}
{α : Type u_2}
[preorder ι]
[topological_space α]
[complete_linear_order α]
[order_topology α]
{f : ι → α} :
monotone f → filter.tendsto f filter.at_top (nhds (⨆ (i : ι), f i))
theorem
tendsto_of_monotone
{ι : Type u_1}
{α : Type u_2}
[preorder ι]
[topological_space α]
[conditionally_complete_linear_order α]
[order_topology α]
{f : ι → α} :
monotone f → (filter.tendsto f filter.at_top filter.at_top ∨ ∃ (l : α), filter.tendsto f filter.at_top (nhds l))
theorem
tendsto_inv_nhds_within_Ioi
{α : Type u}
[ordered_comm_group α]
[topological_space α]
[topological_group α]
{a : α} :
filter.tendsto has_inv.inv (nhds_within a (set.Ioi a)) (nhds_within a⁻¹ (set.Iio a⁻¹))
theorem
tendsto_neg_nhds_within_Ioi
{α : Type u}
[ordered_add_comm_group α]
[topological_space α]
[topological_add_group α]
{a : α} :
filter.tendsto has_neg.neg (nhds_within a (set.Ioi a)) (nhds_within (-a) (set.Iio (-a)))
theorem
tendsto_inv_nhds_within_Iio
{α : Type u}
[ordered_comm_group α]
[topological_space α]
[topological_group α]
{a : α} :
filter.tendsto has_inv.inv (nhds_within a (set.Iio a)) (nhds_within a⁻¹ (set.Ioi a⁻¹))
theorem
tendsto_neg_nhds_within_Iio
{α : Type u}
[ordered_add_comm_group α]
[topological_space α]
[topological_add_group α]
{a : α} :
filter.tendsto has_neg.neg (nhds_within a (set.Iio a)) (nhds_within (-a) (set.Ioi (-a)))
theorem
tendsto_neg_nhds_within_Ioi_neg
{α : Type u}
[ordered_add_comm_group α]
[topological_space α]
[topological_add_group α]
{a : α} :
filter.tendsto has_neg.neg (nhds_within (-a) (set.Ioi (-a))) (nhds_within a (set.Iio a))
theorem
tendsto_inv_nhds_within_Ioi_inv
{α : Type u}
[ordered_comm_group α]
[topological_space α]
[topological_group α]
{a : α} :
filter.tendsto has_inv.inv (nhds_within a⁻¹ (set.Ioi a⁻¹)) (nhds_within a (set.Iio a))
theorem
tendsto_inv_nhds_within_Iio_inv
{α : Type u}
[ordered_comm_group α]
[topological_space α]
[topological_group α]
{a : α} :
filter.tendsto has_inv.inv (nhds_within a⁻¹ (set.Iio a⁻¹)) (nhds_within a (set.Ioi a))
theorem
tendsto_neg_nhds_within_Iio_neg
{α : Type u}
[ordered_add_comm_group α]
[topological_space α]
[topological_add_group α]
{a : α} :
filter.tendsto has_neg.neg (nhds_within (-a) (set.Iio (-a))) (nhds_within a (set.Ioi a))
theorem
nhds_left_sup_nhds_right
{α : Type u}
(a : α)
[topological_space α]
[linear_order α] :
nhds_within a (set.Iic a) ⊔ nhds_within a (set.Ici a) = nhds a
theorem
nhds_left'_sup_nhds_right
{α : Type u}
(a : α)
[topological_space α]
[linear_order α] :
nhds_within a (set.Iio a) ⊔ nhds_within a (set.Ici a) = nhds a
theorem
nhds_left_sup_nhds_right'
{α : Type u}
(a : α)
[topological_space α]
[linear_order α] :
nhds_within a (set.Iic a) ⊔ nhds_within a (set.Ioi a) = nhds a
theorem
continuous_at_iff_continuous_left_right
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[topological_space β]
{a : α}
{f : α → β} :
continuous_at f a ↔ continuous_within_at f (set.Iic a) a ∧ continuous_within_at f (set.Ici a) a
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 : β} :
a < b → continuous_on f (set.Ioo a b) → filter.tendsto f (nhds_within a (set.Ioi a)) (nhds la) → filter.tendsto f (nhds_within b (set.Iio b)) (nhds lb) → continuous_on (extend_from (set.Ioo a b) f) (set.Icc a b)
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 : β} :
a < b → filter.tendsto f (nhds_within a (set.Ioi a)) (nhds 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 : β} :
a < b → filter.tendsto f (nhds_within b (set.Iio b)) (nhds 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 : β} :
a < b → continuous_on f (set.Ioo a b) → filter.tendsto f (nhds_within a (set.Ioi a)) (nhds la) → continuous_on (extend_from (set.Ioo a b) f) (set.Ico a b)
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 : β} :
a < b → continuous_on f (set.Ioo a b) → filter.tendsto f (nhds_within b (set.Iio b)) (nhds lb) → continuous_on (extend_from (set.Ioo a b) f) (set.Ioc a b)
theorem
continuous_within_at_Ioi_iff_Ici
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[linear_order α]
[topological_space β]
{a : α}
{f : α → β} :
continuous_within_at f (set.Ioi a) a ↔ continuous_within_at f (set.Ici a) a
theorem
continuous_within_at_Iio_iff_Iic
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[linear_order α]
[topological_space β]
{a : α}
{f : α → β} :
continuous_within_at f (set.Iio a) a ↔ continuous_within_at f (set.Iic a) a
theorem
continuous_at_iff_continuous_left'_right'
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[topological_space β]
{a : α}
{f : α → β} :
continuous_at f a ↔ continuous_within_at f (set.Iio a) a ∧ continuous_within_at f (set.Ioi a) a