Theory of topology on ordered spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
Implementation notes #
We do not register the order topology as an instance on a preorder (or even on a linear order).
Indeed, on many such spaces, a topology has already been constructed in a different way (think
of the discrete spaces ℕ or ℤ, or ℝ that could inherit a topology as the completion of ℚ),
and is in general not defeq to the one generated by the intervals. We make it available as a
definition preorder.topology α though, that can be registered as an instance when necessary, or
for specific types.
@[class]
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.
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
subtype.order_closed_topology
{α : Type u}
[topological_space α]
[preorder α]
[t : order_closed_topology α]
{p : α → Prop} :
theorem
is_closed_le_prod
{α : Type u}
[topological_space α]
[preorder α]
[t : order_closed_topology α] :
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) :
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 : α} :
@[protected, instance]
def
order_dual.order_closed_topology
{α : Type u}
[topological_space α]
[preorder α]
[t : order_closed_topology α] :
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 (nhds a₁))
(hg : filter.tendsto g b (nhds a₂))
(h : f ≤ᶠ[b] g) :
a₁ ≤ a₂
theorem
tendsto_le_of_eventually_le
{α : 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 (nhds a₁))
(hg : filter.tendsto g b (nhds a₂))
(h : f ≤ᶠ[b] g) :
a₁ ≤ a₂
Alias of le_of_tendsto_of_tendsto.
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 (nhds a₁))
(hg : filter.tendsto g b (nhds 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 (nhds 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 (nhds 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 (nhds 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 (nhds 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) :
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) :
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 ∈ 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 β}
(hs : is_closed s)
(hf : continuous_on f s)
(hg : continuous_on g s) :
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
le_on_closure
{α : Type u}
{β : Type v}
[topological_space α]
[preorder α]
[t : order_closed_topology α]
[topological_space β]
{f g : β → α}
{s : set β}
(h : ∀ (x : β), x ∈ s → f x ≤ g x)
(hf : continuous_on f (closure s))
(hg : continuous_on g (closure s))
⦃x : β⦄
(hx : x ∈ closure s) :
f x ≤ g x
theorem
is_closed.epigraph
{α : Type u}
{β : Type v}
[topological_space α]
[preorder α]
[t : order_closed_topology α]
[topological_space β]
{f : β → α}
{s : set β}
(hs : is_closed s)
(hf : continuous_on f s) :
theorem
is_closed.hypograph
{α : Type u}
{β : Type v}
[topological_space α]
[preorder α]
[t : order_closed_topology α]
[topological_space β]
{f : β → α}
{s : set β}
(hs : is_closed s)
(hf : continuous_on f s) :
theorem
nhds_within_Ici_ne_bot
{α : Type u}
[topological_space α]
[preorder α]
{a b : α}
(H₂ : a ≤ b) :
(nhds_within b (set.Ici a)).ne_bot
@[instance]
theorem
nhds_within_Ici_self_ne_bot
{α : Type u}
[topological_space α]
[preorder α]
(a : α) :
(nhds_within a (set.Ici a)).ne_bot
theorem
nhds_within_Iic_ne_bot
{α : Type u}
[topological_space α]
[preorder α]
{a b : α}
(H : a ≤ b) :
(nhds_within a (set.Iic b)).ne_bot
@[instance]
theorem
nhds_within_Iic_self_ne_bot
{α : Type u}
[topological_space α]
[preorder α]
(a : α) :
(nhds_within a (set.Iic a)).ne_bot
@[protected, instance]
def
order_closed_topology.to_t2_space
{α : Type u}
[topological_space α]
[partial_order α]
[t : order_closed_topology α] :
t2_space α
theorem
is_open_lt_prod
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α] :
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) :
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
Ioo_subset_closure_interior
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α} :
theorem
Iio_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α}
(h : a < b) :
theorem
Ioi_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α}
(h : a < b) :
theorem
Iic_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α}
(h : a < b) :
theorem
Ici_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α}
(h : a < b) :
theorem
Ioo_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b x : α}
(ha : a < x)
(hb : x < b) :
theorem
Ioc_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b x : α}
(ha : a < x)
(hb : x < b) :
theorem
Ico_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b x : α}
(ha : a < x)
(hb : x < b) :
theorem
Icc_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b x : α}
(ha : a < x)
(hb : x < b) :
theorem
eventually_lt_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 (nhds v)) :
theorem
eventually_gt_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 (nhds v)) :
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 (nhds v)) :
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 (nhds v)) :
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 𝓝[>] a and
𝓝[≥] 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) :
set.Ioo a c ∈ nhds_within b (set.Ioi b)
theorem
Ioc_mem_nhds_within_Ioi
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α}
(H : b ∈ set.Ico a c) :
set.Ioc a c ∈ nhds_within b (set.Ioi b)
theorem
Ico_mem_nhds_within_Ioi
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α}
(H : b ∈ set.Ico a c) :
set.Ico a c ∈ nhds_within b (set.Ioi b)
theorem
Icc_mem_nhds_within_Ioi
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α}
(H : b ∈ set.Ico a c) :
set.Icc a c ∈ nhds_within b (set.Ioi b)
@[simp]
theorem
nhds_within_Ioc_eq_nhds_within_Ioi
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α}
(h : 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 : α}
(h : 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 : α → β}
(h : 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 : α → β}
(h : 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 : α}
(H : b ∈ set.Ioc a c) :
set.Ioo a c ∈ nhds_within b (set.Iio b)
theorem
Ico_mem_nhds_within_Iio
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α}
(H : b ∈ set.Ioc a c) :
set.Ico a c ∈ nhds_within b (set.Iio b)
theorem
Ioc_mem_nhds_within_Iio
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α}
(H : b ∈ set.Ioc a c) :
set.Ioc a c ∈ nhds_within b (set.Iio b)
theorem
Icc_mem_nhds_within_Iio
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α}
(H : b ∈ set.Ioc a c) :
set.Icc a c ∈ nhds_within b (set.Iio b)
@[simp]
theorem
nhds_within_Ico_eq_nhds_within_Iio
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α}
(h : 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 : α}
(h : 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 w}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[topological_space γ]
{a b : α}
{f : α → γ}
(h : 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 w}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[topological_space γ]
{a b : α}
{f : α → γ}
(h : 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 : α}
(H : b ∈ set.Ioo a c) :
set.Ioo a c ∈ nhds_within b (set.Ici b)
theorem
Ioc_mem_nhds_within_Ici
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α}
(H : b ∈ set.Ioo a c) :
set.Ioc a c ∈ nhds_within b (set.Ici b)
theorem
Ico_mem_nhds_within_Ici
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α}
(H : b ∈ set.Ico a c) :
set.Ico a c ∈ nhds_within b (set.Ici b)
theorem
Icc_mem_nhds_within_Ici
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α}
(H : b ∈ set.Ico a c) :
set.Icc a c ∈ nhds_within b (set.Ici b)
@[simp]
theorem
nhds_within_Icc_eq_nhds_within_Ici
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α}
(h : 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 : α}
(h : 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 : α → β}
(h : 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 : α → β}
(h : 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 : α}
(H : b ∈ set.Ioo a c) :
set.Ioo a c ∈ nhds_within b (set.Iic b)
theorem
Ico_mem_nhds_within_Iic
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α}
(H : b ∈ set.Ioo a c) :
set.Ico a c ∈ nhds_within b (set.Iic b)
theorem
Ioc_mem_nhds_within_Iic
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α}
(H : b ∈ set.Ioc a c) :
set.Ioc a c ∈ nhds_within b (set.Iic b)
theorem
Icc_mem_nhds_within_Iic
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b c : α}
(H : b ∈ set.Ioc a c) :
set.Icc a c ∈ nhds_within b (set.Iic b)
@[simp]
theorem
nhds_within_Icc_eq_nhds_within_Iic
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α}
(h : 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 : α}
(h : 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 : α → β}
(h : 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 : α → β}
(h : a < b) :
continuous_within_at f (set.Ioc a b) b ↔ continuous_within_at f (set.Iic b) b
theorem
lt_subset_interior_le
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{f g : β → α}
[topological_space β]
(hf : continuous f)
(hg : continuous g) :
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) :
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) :
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 x → f' 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 x → f' x = g' x) :
continuous (λ (x : β), ite (f x ≤ g x) (f' x) (g' x))
theorem
tendsto.eventually_lt
{α : Type u}
{γ : Type w}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{l : filter γ}
{f g : γ → α}
{y z : α}
(hf : filter.tendsto f l (nhds y))
(hg : filter.tendsto g l (nhds z))
(hyz : y < z) :
theorem
continuous_at.eventually_lt
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{f g : β → α}
[topological_space β]
{x₀ : β}
(hf : continuous_at f x₀)
(hg : continuous_at g x₀)
(hfg : 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 : β), linear_order.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 : β), linear_order.max (f b) (g b))
theorem
continuous_min
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α] :
continuous (λ (p : α × α), linear_order.min p.fst p.snd)
theorem
continuous_max
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α] :
continuous (λ (p : α × α), linear_order.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 (nhds a₁))
(hg : filter.tendsto g b (nhds a₂)) :
filter.tendsto (λ (b : β), linear_order.max (f b) (g b)) b (nhds (linear_order.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 (nhds a₁))
(hg : filter.tendsto g b (nhds a₂)) :
filter.tendsto (λ (b : β), linear_order.min (f b) (g b)) b (nhds (linear_order.min a₁ a₂))
theorem
filter.tendsto.max_right
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{f : β → α}
{l : filter β}
{a : α}
(h : filter.tendsto f l (nhds a)) :
filter.tendsto (λ (i : β), linear_order.max a (f i)) l (nhds a)
theorem
filter.tendsto.max_left
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{f : β → α}
{l : filter β}
{a : α}
(h : filter.tendsto f l (nhds a)) :
filter.tendsto (λ (i : β), linear_order.max (f i) a) l (nhds a)
theorem
filter.tendsto_nhds_max_right
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{f : β → α}
{l : filter β}
{a : α}
(h : filter.tendsto f l (nhds_within a (set.Ioi a))) :
filter.tendsto (λ (i : β), linear_order.max a (f i)) l (nhds_within a (set.Ioi a))
theorem
filter.tendsto_nhds_max_left
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{f : β → α}
{l : filter β}
{a : α}
(h : filter.tendsto f l (nhds_within a (set.Ioi a))) :
filter.tendsto (λ (i : β), linear_order.max (f i) a) l (nhds_within a (set.Ioi a))
theorem
filter.tendsto.min_right
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{f : β → α}
{l : filter β}
{a : α}
(h : filter.tendsto f l (nhds a)) :
filter.tendsto (λ (i : β), linear_order.min a (f i)) l (nhds a)
theorem
filter.tendsto.min_left
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{f : β → α}
{l : filter β}
{a : α}
(h : filter.tendsto f l (nhds a)) :
filter.tendsto (λ (i : β), linear_order.min (f i) a) l (nhds a)
theorem
filter.tendsto_nhds_min_right
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{f : β → α}
{l : filter β}
{a : α}
(h : filter.tendsto f l (nhds_within a (set.Iio a))) :
filter.tendsto (λ (i : β), linear_order.min a (f i)) l (nhds_within a (set.Iio a))
theorem
filter.tendsto_nhds_min_left
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{f : β → α}
{l : filter β}
{a : α}
(h : filter.tendsto f l (nhds_within a (set.Iio a))) :
filter.tendsto (λ (i : β), linear_order.min (f i) a) l (nhds_within a (set.Iio a))
theorem
dense.exists_lt
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[no_min_order α]
{s : set α}
(hs : dense s)
(x : α) :
theorem
dense.exists_gt
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[no_max_order α]
{s : set α}
(hs : dense s)
(x : α) :
theorem
dense.exists_le
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[no_min_order α]
{s : set α}
(hs : dense s)
(x : α) :
theorem
dense.exists_ge
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[no_max_order α]
{s : set α}
(hs : dense s)
(x : α) :
theorem
dense.exists_le'
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{s : set α}
(hs : dense s)
(hbot : ∀ (x : α), is_bot x → x ∈ s)
(x : α) :
theorem
dense.exists_ge'
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{s : set α}
(hs : dense s)
(htop : ∀ (x : α), is_top x → x ∈ s)
(x : α) :
theorem
dense.exists_between
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
[densely_ordered α]
{s : set α}
(hs : dense s)
{x y : α}
(h : x < y) :
@[protected, instance]
def
prod.order_closed_topology
{α : Type u}
{β : Type v}
[preorder α]
[topological_space α]
[order_closed_topology α]
[preorder β]
[topological_space β]
[order_closed_topology β] :
order_closed_topology (α × β)
@[protected, instance]
def
pi.order_closed_topology
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), preorder (α i)]
[Π (i : ι), topological_space (α i)]
[∀ (i : ι), order_closed_topology (α i)] :
order_closed_topology (Π (i : ι), α i)
@[protected, instance]
def
pi.order_closed_topology'
{α : Type u}
{β : Type v}
[preorder β]
[topological_space β]
[order_closed_topology β] :
order_closed_topology (α → β)
@[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.
@[protected, instance]
def
order_dual.order_topology
{α : Type u}
[topological_space α]
[preorder α]
[t : order_topology α] :
theorem
is_open_iff_generate_intervals
{α : Type u}
[topological_space α]
[preorder α]
[t : order_topology α]
{s : set α} :
theorem
is_open_lt'
{α : Type u}
[topological_space α]
[preorder α]
[t : order_topology α]
(a : α) :
theorem
is_open_gt'
{α : Type u}
[topological_space α]
[preorder α]
[t : order_topology α]
(a : α) :
theorem
lt_mem_nhds
{α : Type u}
[topological_space α]
[preorder α]
[t : order_topology α]
{a b : α}
(h : a < b) :
theorem
le_mem_nhds
{α : Type u}
[topological_space α]
[preorder α]
[t : order_topology α]
{a b : α}
(h : a < b) :
theorem
gt_mem_nhds
{α : Type u}
[topological_space α]
[preorder α]
[t : order_topology α]
{a b : α}
(h : a < b) :
theorem
ge_mem_nhds
{α : Type u}
[topological_space α]
[preorder α]
[t : order_topology α]
{a b : α}
(h : a < b) :
theorem
nhds_eq_order
{α : Type u}
[topological_space α]
[preorder α]
[t : order_topology α]
(a : α) :
@[protected, instance]
def
tendsto_Icc_class_nhds
{α : Type u}
[topological_space α]
[preorder α]
[t : order_topology α]
(a : α) :
filter.tendsto_Ixx_class set.Icc (nhds a) (nhds a)
@[protected, instance]
def
tendsto_Ico_class_nhds
{α : Type u}
[topological_space α]
[preorder α]
[t : order_topology α]
(a : α) :
filter.tendsto_Ixx_class set.Ico (nhds a) (nhds a)
@[protected, instance]
def
tendsto_Ioc_class_nhds
{α : Type u}
[topological_space α]
[preorder α]
[t : order_topology α]
(a : α) :
filter.tendsto_Ixx_class set.Ioc (nhds a) (nhds a)
@[protected, instance]
def
tendsto_Ioo_class_nhds
{α : Type u}
[topological_space α]
[preorder α]
[t : order_topology α]
(a : α) :
filter.tendsto_Ixx_class set.Ioo (nhds a) (nhds a)
theorem
tendsto_of_tendsto_of_tendsto_of_le_of_le'
{α : Type u}
{β : Type v}
[topological_space α]
[preorder α]
[t : order_topology α]
{f g h : β → α}
{b : filter β}
{a : α}
(hg : filter.tendsto g b (nhds a))
(hh : filter.tendsto h b (nhds a))
(hgf : ∀ᶠ (b : β) in b, g b ≤ f b)
(hfh : ∀ᶠ (b : β) in b, f b ≤ h b) :
filter.tendsto f b (nhds a)
Squeeze theorem (also known as sandwich theorem). This version assumes that inequalities hold eventually for the filter.
theorem
tendsto_of_tendsto_of_tendsto_of_le_of_le
{α : Type u}
{β : Type v}
[topological_space α]
[preorder α]
[t : order_topology α]
{f g h : β → α}
{b : filter β}
{a : α}
(hg : filter.tendsto g b (nhds a))
(hh : filter.tendsto h b (nhds a))
(hgf : g ≤ f)
(hfh : f ≤ h) :
filter.tendsto f b (nhds a)
Squeeze theorem (also known as sandwich theorem). This version assumes that inequalities hold everywhere.
theorem
nhds_order_unbounded
{α : Type u}
[topological_space α]
[preorder α]
[t : order_topology α]
{a : α}
(hu : ∃ (u : α), a < u)
(hl : ∃ (l : α), l < a) :
theorem
tendsto_order_unbounded
{α : Type u}
{β : Type v}
[topological_space α]
[preorder α]
[t : order_topology α]
{f : β → α}
{a : α}
{x : filter β}
(hu : ∃ (u : α), a < u)
(hl : ∃ (l : α), l < a)
(h : ∀ (l u : α), l < a → a < u → (∀ᶠ (b : β) in x, l < f b ∧ f b < u)) :
filter.tendsto f x (nhds a)
@[protected, instance]
def
tendsto_Ixx_nhds_within
{α : Type u_1}
[preorder α]
[topological_space α]
(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)
@[protected, instance]
def
tendsto_Icc_class_nhds_pi
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), preorder (α i)]
[Π (i : ι), topological_space (α i)]
[∀ (i : ι), order_topology (α i)]
(f : Π (i : ι), α i) :
filter.tendsto_Ixx_class set.Icc (nhds f) (nhds f)
theorem
induced_order_topology'
{α : Type u}
{β : Type v}
[preorder α]
[ta : topological_space β]
[preorder β]
[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)) :
@[protected, instance]
def
order_topology_of_ord_connected
{α : Type u}
[ta : topological_space α]
[linear_order α]
[order_topology α]
{t : set α}
[ht : t.ord_connected] :
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_within_Ici_eq''
{α : Type u}
[topological_space α]
[preorder α]
[order_topology α]
(a : α) :
nhds_within a (set.Ici a) = (⨅ (u : α) (hu : a < u), filter.principal (set.Iio u)) ⊓ filter.principal (set.Ici a)
theorem
nhds_within_Iic_eq''
{α : Type u}
[topological_space α]
[preorder α]
[order_topology α]
(a : α) :
nhds_within a (set.Iic a) = (⨅ (l : α) (H : l < a), filter.principal (set.Ioi l)) ⊓ filter.principal (set.Iic a)
theorem
nhds_within_Ici_eq'
{α : Type u}
[topological_space α]
[preorder α]
[order_topology α]
{a : α}
(ha : ∃ (u : α), a < u) :
nhds_within a (set.Ici a) = ⨅ (u : α) (hu : a < u), filter.principal (set.Ico a u)
theorem
nhds_within_Iic_eq'
{α : Type u}
[topological_space α]
[preorder α]
[order_topology α]
{a : α}
(ha : ∃ (l : α), l < a) :
nhds_within a (set.Iic a) = ⨅ (l : α) (H : l < a), filter.principal (set.Ioc l a)
theorem
nhds_within_Ici_basis'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
(ha : ∃ (u : α), a < u) :
(nhds_within a (set.Ici a)).has_basis (λ (u : α), a < u) (λ (u : α), set.Ico a u)
theorem
nhds_within_Iic_basis'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
(ha : ∃ (l : α), l < a) :
(nhds_within a (set.Iic a)).has_basis (λ (l : α), l < a) (λ (l : α), set.Ioc l a)
theorem
nhds_within_Ici_basis
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[no_max_order α]
(a : α) :
(nhds_within a (set.Ici a)).has_basis (λ (u : α), a < u) (λ (u : α), set.Ico a u)
theorem
nhds_within_Iic_basis
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[no_min_order α]
(a : α) :
(nhds_within a (set.Iic a)).has_basis (λ (l : α), l < a) (λ (l : α), set.Ioc l a)
theorem
nhds_top_order
{α : Type u}
[topological_space α]
[preorder α]
[order_top α]
[order_topology α] :
theorem
nhds_bot_order
{α : Type u}
[topological_space α]
[preorder α]
[order_bot α]
[order_topology α] :
theorem
nhds_top_basis
{α : Type u}
[topological_space α]
[linear_order α]
[order_top α]
[order_topology α]
[nontrivial α] :
theorem
nhds_bot_basis
{α : Type u}
[topological_space α]
[linear_order α]
[order_bot α]
[order_topology α]
[nontrivial α] :
theorem
nhds_top_basis_Ici
{α : Type u}
[topological_space α]
[linear_order α]
[order_top α]
[order_topology α]
[nontrivial α]
[densely_ordered α] :
theorem
nhds_bot_basis_Iic
{α : Type u}
[topological_space α]
[linear_order α]
[order_bot α]
[order_topology α]
[nontrivial α]
[densely_ordered α] :
theorem
tendsto_nhds_top_mono
{α : Type u}
{β : Type v}
[topological_space β]
[preorder β]
[order_top β]
[order_topology β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l (nhds ⊤))
(hg : f ≤ᶠ[l] g) :
filter.tendsto g l (nhds ⊤)
theorem
tendsto_nhds_bot_mono
{α : Type u}
{β : Type v}
[topological_space β]
[preorder β]
[order_bot β]
[order_topology β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l (nhds ⊥))
(hg : g ≤ᶠ[l] f) :
filter.tendsto g l (nhds ⊥)
theorem
tendsto_nhds_top_mono'
{α : Type u}
{β : Type v}
[topological_space β]
[preorder β]
[order_top β]
[order_topology β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l (nhds ⊤))
(hg : f ≤ g) :
filter.tendsto g l (nhds ⊤)
theorem
tendsto_nhds_bot_mono'
{α : Type u}
{β : Type v}
[topological_space β]
[preorder β]
[order_bot β]
[order_topology β]
{l : filter α}
{f g : α → β}
(hf : filter.tendsto f l (nhds ⊥))
(hg : g ≤ f) :
filter.tendsto g l (nhds ⊥)
theorem
eventually_le_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α}
(hab : a < b) :
theorem
eventually_lt_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α}
(hab : a < b) :
theorem
eventually_ge_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α}
(hab : b < a) :
theorem
eventually_gt_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_closed_topology α]
{a b : α}
(hab : b < a) :
@[protected, instance]
def
order_topology.to_order_closed_topology
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α] :
theorem
exists_Ioc_subset_of_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α}
(hs : s ∈ nhds a)
(h : ∃ (l : α), l < a) :
theorem
exists_Ioc_subset_of_mem_nhds'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α}
(hs : s ∈ nhds a)
{l : α}
(hl : l < a) :
theorem
exists_Ico_subset_of_mem_nhds'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α}
(hs : s ∈ nhds a)
{u : α}
(hu : a < u) :
theorem
exists_Ico_subset_of_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α}
(hs : s ∈ nhds a)
(h : ∃ (u : α), a < u) :
theorem
exists_Icc_mem_subset_of_mem_nhds_within_Ici
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α}
(hs : s ∈ nhds_within a (set.Ici a)) :
theorem
exists_Icc_mem_subset_of_mem_nhds_within_Iic
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α}
(hs : s ∈ nhds_within a (set.Iic a)) :
theorem
exists_Icc_mem_subset_of_mem_nhds
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α}
(hs : s ∈ nhds a) :
theorem
is_open.exists_Ioo_subset
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[nontrivial α]
{s : set α}
(hs : is_open s)
(h : s.nonempty) :
theorem
dense_of_exists_between
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[nontrivial α]
{s : set α}
(h : ∀ ⦃a b : α⦄, a < b → (∃ (c : α) (H : c ∈ s), a < c ∧ c < b)) :
dense s
theorem
dense_iff_exists_between
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[nontrivial α]
{s : set α} :
A set in a nontrivial densely linear ordered type is dense in the sense of topology if and only
if for any a < b there exists c ∈ s, a < c < b. Each implication requires less typeclass
assumptions.
theorem
mem_nhds_iff_exists_Ioo_subset'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α}
(hl : ∃ (l : α), l < a)
(hu : ∃ (u : α), a < u) :
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_max_order α]
[no_min_order α]
{a : α}
{s : set α} :
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 α]
[no_max_order α]
[no_min_order α]
(a : α) :
theorem
filter.eventually.exists_Ioo_subset
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[no_max_order α]
[no_min_order α]
{a : α}
{p : α → Prop}
(hp : ∀ᶠ (x : α) in nhds a, p x) :
theorem
countable_of_isolated_right
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α] :
The set of points which are isolated on the right is countable when the space is second-countable.
theorem
countable_of_isolated_left
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α] :
The set of points which are isolated on the left is countable when the space is second-countable.
theorem
set.pairwise_disjoint.countable_of_Ioo
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[topological_space.second_countable_topology α]
{y : α → α}
{s : set α}
(h : s.pairwise_disjoint (λ (x : α), set.Ioo x (y x)))
(h' : ∀ (x : α), x ∈ s → x < y x) :
Consider a disjoint family of intervals (x, y) with x < y in a second-countable space.
Then the family is countable.
This is not a straightforward consequence of second-countability as some of these intervals might be
empty (but in fact this can happen only for countably many of them).
Intervals in Π i, π i belong to 𝓝 x #
For each lemma pi_Ixx_mem_nhds we add a non-dependent version pi_Ixx_mem_nhds' because
sometimes Lean fails to unify different instances while trying to apply the dependent version to,
e.g., ι → ℝ.
theorem
pi_Iic_mem_nhds
{ι : Type u_1}
{π : ι → Type u_2}
[finite ι]
[Π (i : ι), 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}
[finite ι]
{a' x' : ι → α}
(ha : ∀ (i : ι), x' i < a' i) :
theorem
pi_Ici_mem_nhds
{ι : Type u_1}
{π : ι → Type u_2}
[finite ι]
[Π (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}
[finite ι]
{a' x' : ι → α}
(ha : ∀ (i : ι), a' i < x' i) :
theorem
pi_Icc_mem_nhds
{ι : Type u_1}
{π : ι → Type u_2}
[finite ι]
[Π (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}
[finite ι]
{a' b' x' : ι → α}
(ha : ∀ (i : ι), a' i < x' i)
(hb : ∀ (i : ι), x' i < b' i) :
theorem
pi_Iio_mem_nhds
{ι : Type u_1}
{π : ι → Type u_2}
[finite ι]
[Π (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}
[finite ι]
{a' x' : ι → α}
[nonempty ι]
(ha : ∀ (i : ι), x' i < a' i) :
theorem
pi_Ioi_mem_nhds
{ι : Type u_1}
{π : ι → Type u_2}
[finite ι]
[Π (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}
[finite ι]
{a' x' : ι → α}
[nonempty ι]
(ha : ∀ (i : ι), a' i < x' i) :
theorem
pi_Ioc_mem_nhds'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{ι : Type u_1}
[finite ι]
{a' b' x' : ι → α}
[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}
[finite ι]
{a' b' x' : ι → α}
[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}
[finite ι]
{a' b' x' : ι → α}
[nonempty ι]
(ha : ∀ (i : ι), a' i < x' i)
(hb : ∀ (i : ι), x' i < b' i) :
theorem
disjoint_nhds_at_top
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[no_max_order α]
(x : α) :
@[simp]
theorem
inf_nhds_at_top
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[no_max_order α]
(x : α) :
nhds x ⊓ filter.at_top = ⊥
theorem
disjoint_nhds_at_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[no_min_order α]
(x : α) :
@[simp]
theorem
inf_nhds_at_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[no_min_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_max_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_max_order α]
{F : filter β}
[F.ne_bot]
{f : β → α}
{x : α}
(hf : filter.tendsto f F (nhds x)) :
theorem
not_tendsto_nhds_of_tendsto_at_bot
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_topology α]
[no_min_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_min_order α]
{F : filter β}
[F.ne_bot]
{f : β → α}
{x : α}
(hf : filter.tendsto f F (nhds 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 α) :
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 α}
(hu' : a < u') :
theorem
mem_nhds_within_Ioi_iff_exists_Ioo_subset'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a u' : α}
{s : set α}
(hu' : a < u') :
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_max_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_max_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 α}
(hl' : l' < a) :
theorem
mem_nhds_within_Iio_iff_exists_Ioo_subset'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a l' : α}
{s : set α}
(hl' : l' < a) :
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_min_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_min_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 α}
(hu' : a < u') :
theorem
mem_nhds_within_Ici_iff_exists_Ico_subset'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a u' : α}
{s : set α}
(hu' : a < u') :
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_max_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
nhds_within_Ici_basis_Ico
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[no_max_order α]
(a : α) :
(nhds_within a (set.Ici a)).has_basis (λ (u : α), a < u) (set.Ico a)
theorem
mem_nhds_within_Ici_iff_exists_Icc_subset
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[no_max_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 α}
(hl' : l' < a) :
theorem
mem_nhds_within_Iic_iff_exists_Ioc_subset'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a l' : α}
{s : set α}
(hl' : l' < a) :
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_min_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_min_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
nhds_eq_infi_abs_sub
{α : Type u}
[topological_space α]
[linear_ordered_add_comm_group α]
[order_topology α]
(a : α) :
theorem
order_topology_of_nhds_abs
{α : Type u_1}
[topological_space α]
[linear_ordered_add_comm_group α]
(h_nhds : ∀ (a : α), nhds a = ⨅ (r : α) (H : r > 0), filter.principal {b : α | |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 : α} :
theorem
eventually_abs_sub_lt
{α : Type u}
[topological_space α]
[linear_ordered_add_comm_group α]
[order_topology α]
(a : α)
{ε : α}
(hε : 0 < ε) :
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 (nhds 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 (nhds 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 (nhds 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 (nhds 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
nhds_basis_Ioo_pos
{α : Type u}
[topological_space α]
[linear_ordered_add_comm_group α]
[order_topology α]
[no_min_order α]
[no_max_order α]
(a : α) :
theorem
nhds_basis_abs_sub_lt
{α : Type u}
[topological_space α]
[linear_ordered_add_comm_group α]
[order_topology α]
[no_min_order α]
[no_max_order α]
(a : α) :
theorem
nhds_basis_zero_abs_sub_lt
(α : Type u)
[topological_space α]
[linear_ordered_add_comm_group α]
[order_topology α]
[no_min_order α]
[no_max_order α] :
theorem
nhds_basis_Ioo_pos_of_pos
{α : Type u}
[topological_space α]
[linear_ordered_add_comm_group α]
[order_topology α]
[no_min_order α]
[no_max_order α]
{a : α}
(ha : 0 < a) :
If a is positive we can form a basis from only nonnegative Ioo intervals
theorem
is_lub.frequently_mem
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α}
(ha : is_lub s a)
(hs : s.nonempty) :
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) :
theorem
is_glb.frequently_mem
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α}
(ha : is_glb s a)
(hs : s.nonempty) :
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) :
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) :
(nhds_within a s).ne_bot
theorem
is_glb.nhds_within_ne_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{a : α}
{s : set α} :
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_lub_of_mem_closure
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{s : set α}
{a : α}
(hsa : a ∈ upper_bounds s)
(hsf : a ∈ closure s) :
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_glb_of_mem_closure
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{s : set α}
{a : α}
(hsa : a ∈ lower_bounds s)
(hsf : a ∈ closure s) :
is_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 : monotone_on f s)
(ha : is_lub s a)
(hb : filter.tendsto f (nhds_within a s) (nhds b)) :
b ∈ upper_bounds (f '' s)
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 : monotone_on f s)
(ha : is_lub s a)
(hs : s.nonempty)
(hb : filter.tendsto f (nhds_within a s) (nhds 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 : monotone_on f s)
(ha : is_glb s a)
(hb : filter.tendsto f (nhds_within a s) (nhds b)) :
b ∈ lower_bounds (f '' s)
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 : monotone_on f s) :
is_glb s a → s.nonempty → filter.tendsto f (nhds_within a s) (nhds 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 : antitone_on f s)
(ha : is_lub s a)
(hb : filter.tendsto f (nhds_within a s) (nhds b)) :
b ∈ lower_bounds (f '' s)
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 : γ} :
antitone_on f s → is_lub s a → s.nonempty → filter.tendsto f (nhds_within a s) (nhds 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 : antitone_on f s)
(ha : is_glb s a)
(hb : filter.tendsto f (nhds_within a s) (nhds b)) :
b ∈ upper_bounds (f '' s)
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 : γ} :
antitone_on f s → is_glb s a → s.nonempty → filter.tendsto f (nhds_within a s) (nhds 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.
Existence of sequences tending to Inf or Sup of a given set #
theorem
is_lub.exists_seq_strict_mono_tendsto_of_not_mem
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{t : set α}
{x : α}
[(nhds x).is_countably_generated]
(htx : is_lub t x)
(not_mem : x ∉ t)
(ht : t.nonempty) :
theorem
is_lub.exists_seq_monotone_tendsto
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{t : set α}
{x : α}
[(nhds x).is_countably_generated]
(htx : is_lub t x)
(ht : t.nonempty) :
theorem
exists_seq_strict_mono_tendsto'
{α : Type u_1}
[linear_order α]
[topological_space α]
[densely_ordered α]
[order_topology α]
[topological_space.first_countable_topology α]
{x y : α}
(hy : y < x) :
∃ (u : ℕ → α), strict_mono u ∧ (∀ (n : ℕ), u n ∈ set.Ioo y x) ∧ filter.tendsto u filter.at_top (nhds x)
theorem
exists_seq_strict_mono_tendsto
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_min_order α]
[topological_space.first_countable_topology α]
(x : α) :
∃ (u : ℕ → α), strict_mono u ∧ (∀ (n : ℕ), u n < x) ∧ filter.tendsto u filter.at_top (nhds x)
theorem
exists_seq_strict_mono_tendsto_nhds_within
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_min_order α]
[topological_space.first_countable_topology α]
(x : α) :
∃ (u : ℕ → α), strict_mono u ∧ (∀ (n : ℕ), u n < x) ∧ filter.tendsto u filter.at_top (nhds_within x (set.Iio x))
theorem
exists_seq_tendsto_Sup
{α : Type u_1}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[topological_space.first_countable_topology α]
{S : set α}
(hS : S.nonempty)
(hS' : bdd_above S) :
∃ (u : ℕ → α), monotone u ∧ filter.tendsto u filter.at_top (nhds (has_Sup.Sup S)) ∧ ∀ (n : ℕ), u n ∈ S
theorem
is_glb.exists_seq_strict_anti_tendsto_of_not_mem
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{t : set α}
{x : α}
[(nhds x).is_countably_generated]
(htx : is_glb t x)
(not_mem : x ∉ t)
(ht : t.nonempty) :
theorem
is_glb.exists_seq_antitone_tendsto
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
{t : set α}
{x : α}
[(nhds x).is_countably_generated]
(htx : is_glb t x)
(ht : t.nonempty) :
theorem
exists_seq_strict_anti_tendsto'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[topological_space.first_countable_topology α]
{x y : α}
(hy : x < y) :
∃ (u : ℕ → α), strict_anti u ∧ (∀ (n : ℕ), u n ∈ set.Ioo x y) ∧ filter.tendsto u filter.at_top (nhds x)
theorem
exists_seq_strict_anti_tendsto
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_max_order α]
[topological_space.first_countable_topology α]
(x : α) :
∃ (u : ℕ → α), strict_anti u ∧ (∀ (n : ℕ), x < u n) ∧ filter.tendsto u filter.at_top (nhds x)
theorem
exists_seq_strict_anti_tendsto_nhds_within
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_max_order α]
[topological_space.first_countable_topology α]
(x : α) :
∃ (u : ℕ → α), strict_anti u ∧ (∀ (n : ℕ), x < u n) ∧ filter.tendsto u filter.at_top (nhds_within x (set.Ioi x))
theorem
exists_seq_strict_anti_strict_mono_tendsto
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[topological_space.first_countable_topology α]
{x y : α}
(h : x < y) :
∃ (u v : ℕ → α), strict_anti u ∧ strict_mono v ∧ (∀ (k : ℕ), u k ∈ set.Ioo x y) ∧ (∀ (l : ℕ), v l ∈ set.Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ filter.tendsto u filter.at_top (nhds x) ∧ filter.tendsto v filter.at_top (nhds y)
theorem
exists_seq_tendsto_Inf
{α : Type u_1}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[topological_space.first_countable_topology α]
{S : set α}
(hS : S.nonempty)
(hS' : bdd_below S) :
∃ (u : ℕ → α), antitone u ∧ filter.tendsto u filter.at_top (nhds (has_Inf.Inf S)) ∧ ∀ (n : ℕ), u n ∈ S
theorem
closure_Ioi'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a : α}
(h : (set.Ioi a).nonempty) :
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_max_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 : α}
(h : (set.Iio a).nonempty) :
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_min_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 α]
{a : α}
(ha : (set.Iio a).nonempty) :
theorem
interior_Ici
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_min_order α]
{a : α} :
@[simp]
theorem
interior_Iic'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a : α}
(ha : (set.Ioi a).nonempty) :
theorem
interior_Iic
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_max_order α]
{a : α} :
@[simp]
theorem
interior_Icc
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_min_order α]
[no_max_order α]
{a b : α} :
@[simp]
theorem
interior_Ico
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_min_order α]
{a b : α} :
@[simp]
theorem
interior_Ioc
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_max_order α]
{a b : α} :
theorem
closure_interior_Icc
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a b : α}
(h : a ≠ b) :
theorem
Ioc_subset_closure_interior
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
(a b : α) :
theorem
Ico_subset_closure_interior
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
(a b : α) :
@[simp]
theorem
frontier_Ici'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a : α}
(ha : (set.Iio a).nonempty) :
theorem
frontier_Ici
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_min_order α]
{a : α} :
@[simp]
theorem
frontier_Iic'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a : α}
(ha : (set.Ioi a).nonempty) :
theorem
frontier_Iic
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_max_order α]
{a : α} :
@[simp]
theorem
frontier_Ioi'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a : α}
(ha : (set.Ioi a).nonempty) :
theorem
frontier_Ioi
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_max_order α]
{a : α} :
@[simp]
theorem
frontier_Iio'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a : α}
(ha : (set.Iio a).nonempty) :
theorem
frontier_Iio
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_min_order α]
{a : α} :
@[simp]
theorem
frontier_Icc
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_min_order α]
[no_max_order α]
{a b : α}
(h : a ≤ b) :
@[simp]
theorem
frontier_Ioo
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a b : α}
(h : a < b) :
@[simp]
theorem
frontier_Ico
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_min_order α]
{a b : α}
(h : a < b) :
@[simp]
theorem
frontier_Ioc
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_max_order α]
{a b : α}
(h : a < b) :
theorem
nhds_within_Ioi_ne_bot'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a b : α}
(H₁ : (set.Ioi a).nonempty)
(H₂ : 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_max_order α]
{a b : α}
(H : 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 : α}
(H : (set.Ioi a).nonempty) :
(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_max_order α]
(a : α) :
(nhds_within a (set.Ioi a)).ne_bot
theorem
filter.eventually.exists_gt
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_max_order α]
{a : α}
{p : α → Prop}
(h : ∀ᶠ (x : α) in nhds a, p x) :
theorem
nhds_within_Iio_ne_bot'
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{b c : α}
(H₁ : (set.Iio c).nonempty)
(H₂ : 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_min_order α]
{a b : α}
(H : 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 α]
{b : α}
(H : (set.Iio b).nonempty) :
(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_min_order α]
(a : α) :
(nhds_within a (set.Iio a)).ne_bot
theorem
filter.eventually.exists_lt
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[no_min_order α]
{a : α}
{p : α → Prop}
(h : ∀ᶠ (x : α) in nhds a, p x) :
theorem
right_nhds_within_Ico_ne_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a b : α}
(H : a < b) :
(nhds_within b (set.Ico a b)).ne_bot
theorem
left_nhds_within_Ioc_ne_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a b : α}
(H : a < b) :
(nhds_within a (set.Ioc a b)).ne_bot
theorem
left_nhds_within_Ioo_ne_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a b : α}
(H : a < b) :
(nhds_within a (set.Ioo a b)).ne_bot
theorem
right_nhds_within_Ioo_ne_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a b : α}
(H : a < b) :
(nhds_within b (set.Ioo a b)).ne_bot
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)) :
filter.comap coe (nhds_within b (set.Iio b)) = filter.at_top
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)) :
filter.comap coe (nhds_within a (set.Ioi a)) = filter.at_bot
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)) :
theorem
comap_coe_Ioo_nhds_within_Iio
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
(a b : α) :
filter.comap coe (nhds_within b (set.Iio b)) = filter.at_top
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.
theorem
comap_coe_Ioo_nhds_within_Ioi
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
(a b : α) :
filter.comap coe (nhds_within a (set.Ioi a)) = filter.at_bot
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.
theorem
comap_coe_Ioi_nhds_within_Ioi
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
(a : α) :
filter.comap coe (nhds_within a (set.Ioi a)) = filter.at_bot
theorem
comap_coe_Iio_nhds_within_Iio
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
(a : α) :
filter.comap coe (nhds_within a (set.Iio a)) = filter.at_top
@[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
map_coe_Ioi_at_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
(a : α) :
@[simp]
theorem
map_coe_Iio_at_top
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
(a : α) :
@[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) :
filter.tendsto (λ (x : ↥(set.Ioo a b)), f ↑x) filter.at_top l ↔ filter.tendsto f (nhds_within b (set.Iio b)) l
@[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) :
filter.tendsto (λ (x : ↥(set.Ioo a b)), f ↑x) filter.at_bot l ↔ filter.tendsto f (nhds_within a (set.Ioi a)) l
@[simp]
theorem
tendsto_comp_coe_Ioi_at_bot
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a : α}
{l : filter β}
{f : α → β} :
filter.tendsto (λ (x : ↥(set.Ioi a)), f ↑x) filter.at_bot l ↔ filter.tendsto f (nhds_within a (set.Ioi a)) l
@[simp]
theorem
tendsto_comp_coe_Iio_at_top
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
{a : α}
{l : filter β}
{f : α → β} :
filter.tendsto (λ (x : ↥(set.Iio a)), f ↑x) filter.at_top l ↔ filter.tendsto f (nhds_within a (set.Iio a)) l
@[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)} :
filter.tendsto f l filter.at_top ↔ filter.tendsto (λ (x : β), ↑(f x)) l (nhds_within b (set.Iio 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)} :
filter.tendsto f l filter.at_bot ↔ filter.tendsto (λ (x : β), ↑(f x)) l (nhds_within a (set.Ioi a))
@[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)} :
filter.tendsto f l filter.at_bot ↔ filter.tendsto (λ (x : β), ↑(f x)) l (nhds_within a (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)} :
filter.tendsto f l filter.at_top ↔ filter.tendsto (λ (x : β), ↑(f x)) l (nhds_within a (set.Iio a))
@[protected, instance]
def
nhds_within.filter.ne_bot
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
(x : α)
[nontrivial α] :
(nhds_within x {x}ᶜ).ne_bot
theorem
dense.exists_countable_dense_subset_no_bot_top
{α : Type u}
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[nontrivial α]
{s : set α}
[topological_space.separable_space ↥s]
(hs : dense s) :
Let s be a dense set in a nontrivial dense linear order α. If s is a
separable space (e.g., if α has a second countable topology), then there exists a countable
dense subset t ⊆ s such that t does not contain bottom/top elements of α.
theorem
exists_countable_dense_no_bot_top
(α : Type u)
[topological_space α]
[linear_order α]
[order_topology α]
[densely_ordered α]
[topological_space.separable_space α]
[nontrivial α] :
If α is a nontrivial separable dense linear order, then there exists a
countable dense set s : set α that contains neither top nor bottom elements of α.
For a dense set containing both bot and top elements, see
exists_countable_dense_bot_top.
theorem
Sup_mem_closure
{α : Type u}
[topological_space α]
[complete_linear_order α]
[order_topology α]
{s : set α}
(hs : s.nonempty) :
has_Sup.Sup s ∈ closure s
theorem
Inf_mem_closure
{α : Type u}
[topological_space α]
[complete_linear_order α]
[order_topology α]
{s : set α}
(hs : s.nonempty) :
has_Inf.Inf s ∈ closure s
theorem
is_closed.Sup_mem
{α : Type u}
[topological_space α]
[complete_linear_order α]
[order_topology α]
{s : set α}
(hs : s.nonempty)
(hc : is_closed s) :
has_Sup.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) :
has_Inf.Inf s ∈ s
theorem
monotone.map_Sup_of_continuous_at'
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{f : α → β}
{s : set α}
(Cf : continuous_at f (has_Sup.Sup s))
(Mf : monotone f)
(hs : 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
monotone.map_Sup_of_continuous_at
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{f : α → β}
{s : set α}
(Cf : continuous_at f (has_Sup.Sup s))
(Mf : monotone f)
(fbot : f ⊥ = ⊥) :
f (has_Sup.Sup s) = has_Sup.Sup (f '' s)
A monotone function f sending bot to bot and continuous at the supremum of a set sends
this supremum to the supremum of the image of this set.
theorem
monotone.map_supr_of_continuous_at'
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{ι : Sort u_1}
[nonempty ι]
{f : α → β}
{g : ι → α}
(Cf : continuous_at f (supr g))
(Mf : monotone f) :
A monotone function continuous at the indexed supremum over a nonempty Sort sends this indexed
supremum to the indexed supremum of the composition.
theorem
monotone.map_supr_of_continuous_at
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{ι : Sort u_1}
{f : α → β}
{g : ι → α}
(Cf : continuous_at f (supr g))
(Mf : monotone f)
(fbot : f ⊥ = ⊥) :
If a monotone function sending bot to bot is continuous at the indexed supremum over
a Sort, then it sends this indexed supremum to the indexed supremum of the composition.
theorem
monotone.map_Inf_of_continuous_at'
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{f : α → β}
{s : set α}
(Cf : continuous_at f (has_Inf.Inf s))
(Mf : monotone f)
(hs : 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
monotone.map_Inf_of_continuous_at
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{f : α → β}
{s : set α}
(Cf : continuous_at f (has_Inf.Inf s))
(Mf : monotone f)
(ftop : f ⊤ = ⊤) :
f (has_Inf.Inf s) = has_Inf.Inf (f '' s)
A monotone function f sending top to top and continuous at the infimum of a set sends
this infimum to the infimum of the image of this set.
theorem
monotone.map_infi_of_continuous_at'
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{ι : Sort u_1}
[nonempty ι]
{f : α → β}
{g : ι → α}
(Cf : continuous_at f (infi g))
(Mf : monotone f) :
A monotone function continuous at the indexed infimum over a nonempty Sort sends this indexed
infimum to the indexed infimum of the composition.
theorem
monotone.map_infi_of_continuous_at
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{ι : Sort u_1}
{f : α → β}
{g : ι → α}
(Cf : continuous_at f (infi g))
(Mf : monotone f)
(ftop : f ⊤ = ⊤) :
If a monotone function sending top to top is continuous at the indexed infimum over
a Sort, then it sends this indexed infimum to the indexed infimum of the composition.
theorem
antitone.map_Sup_of_continuous_at'
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{f : α → β}
{s : set α}
(Cf : continuous_at f (has_Sup.Sup s))
(Af : antitone f)
(hs : s.nonempty) :
f (has_Sup.Sup s) = has_Inf.Inf (f '' s)
An antitone function continuous at the supremum of a nonempty set sends this supremum to the infimum of the image of this set.
theorem
antitone.map_Sup_of_continuous_at
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{f : α → β}
{s : set α}
(Cf : continuous_at f (has_Sup.Sup s))
(Af : antitone f)
(fbot : f ⊥ = ⊤) :
f (has_Sup.Sup s) = has_Inf.Inf (f '' s)
An antitone function f sending bot to top and continuous at the supremum of a set sends
this supremum to the infimum of the image of this set.
theorem
antitone.map_supr_of_continuous_at'
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{ι : Sort u_1}
[nonempty ι]
{f : α → β}
{g : ι → α}
(Cf : continuous_at f (supr g))
(Af : antitone f) :
An antitone function continuous at the indexed supremum over a nonempty Sort sends this
indexed supremum to the indexed infimum of the composition.
theorem
antitone.map_supr_of_continuous_at
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{ι : Sort u_1}
{f : α → β}
{g : ι → α}
(Cf : continuous_at f (supr g))
(Af : antitone f)
(fbot : f ⊥ = ⊤) :
An antitone function sending bot to top is continuous at the indexed supremum over
a Sort, then it sends this indexed supremum to the indexed supremum of the composition.
theorem
antitone.map_Inf_of_continuous_at'
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{f : α → β}
{s : set α}
(Cf : continuous_at f (has_Inf.Inf s))
(Af : antitone f)
(hs : s.nonempty) :
f (has_Inf.Inf s) = has_Sup.Sup (f '' s)
An antitone function continuous at the infimum of a nonempty set sends this infimum to the supremum of the image of this set.
theorem
antitone.map_Inf_of_continuous_at
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{f : α → β}
{s : set α}
(Cf : continuous_at f (has_Inf.Inf s))
(Af : antitone f)
(ftop : f ⊤ = ⊥) :
f (has_Inf.Inf s) = has_Sup.Sup (f '' s)
An antitone function f sending top to bot and continuous at the infimum of a set sends
this infimum to the supremum of the image of this set.
theorem
antitone.map_infi_of_continuous_at'
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{ι : Sort u_1}
[nonempty ι]
{f : α → β}
{g : ι → α}
(Cf : continuous_at f (infi g))
(Af : antitone f) :
An antitone function continuous at the indexed infimum over a nonempty Sort sends this indexed
infimum to the indexed supremum of the composition.
theorem
antitone.map_infi_of_continuous_at
{α : Type u}
{β : Type v}
[complete_linear_order α]
[topological_space α]
[order_topology α]
[complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{ι : Sort u_1}
{f : α → β}
{g : ι → α}
(Cf : continuous_at f (infi g))
(Af : antitone f)
(ftop : f ⊤ = ⊥) :
If an antitone function sending top to bot is continuous at the indexed infimum over
a Sort, then it sends this indexed infimum to the indexed supremum of the composition.
theorem
cSup_mem_closure
{α : Type u}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α}
(hs : s.nonempty)
(B : 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 α}
(hs : s.nonempty)
(B : 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 α}
(hc : is_closed s)
(hs : s.nonempty)
(B : 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 α}
(hc : is_closed s)
(hs : s.nonempty)
(B : bdd_below s) :
has_Inf.Inf s ∈ s
theorem
monotone.map_cSup_of_continuous_at
{α : Type u}
{β : Type v}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{f : α → β}
{s : set α}
(Cf : continuous_at f (has_Sup.Sup s))
(Mf : monotone f)
(ne : s.nonempty)
(H : 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
monotone.map_csupr_of_continuous_at
{α : Type u}
{β : Type v}
{γ : Type w}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_closed_topology β]
[nonempty γ]
{f : α → β}
{g : γ → α}
(Cf : continuous_at f (⨆ (i : γ), g i))
(Mf : monotone f)
(H : bdd_above (set.range g)) :
If a monotone function is continuous at the indexed supremum of a bounded function on
a nonempty Sort, then it sends this supremum to the supremum of the composition.
theorem
monotone.map_cInf_of_continuous_at
{α : Type u}
{β : Type v}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{f : α → β}
{s : set α}
(Cf : continuous_at f (has_Inf.Inf s))
(Mf : monotone f)
(ne : s.nonempty)
(H : 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
monotone.map_cinfi_of_continuous_at
{α : Type u}
{β : Type v}
{γ : Type w}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_closed_topology β]
[nonempty γ]
{f : α → β}
{g : γ → α}
(Cf : continuous_at f (⨅ (i : γ), g i))
(Mf : monotone f)
(H : bdd_below (set.range g)) :
A continuous monotone function sends indexed infimum to indexed infimum in conditionally complete linear order, under a boundedness assumption.
theorem
antitone.map_cSup_of_continuous_at
{α : Type u}
{β : Type v}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{f : α → β}
{s : set α}
(Cf : continuous_at f (has_Sup.Sup s))
(Af : antitone f)
(ne : s.nonempty)
(H : bdd_above s) :
f (has_Sup.Sup s) = has_Inf.Inf (f '' s)
If an antitone function is continuous at the supremum of a nonempty bounded above set s,
then it sends this supremum to the infimum of the image of s.
theorem
antitone.map_csupr_of_continuous_at
{α : Type u}
{β : Type v}
{γ : Type w}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_closed_topology β]
[nonempty γ]
{f : α → β}
{g : γ → α}
(Cf : continuous_at f (⨆ (i : γ), g i))
(Af : antitone f)
(H : bdd_above (set.range g)) :
If an antitone function is continuous at the indexed supremum of a bounded function on
a nonempty Sort, then it sends this supremum to the infimum of the composition.
theorem
antitone.map_cInf_of_continuous_at
{α : Type u}
{β : Type v}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_closed_topology β]
{f : α → β}
{s : set α}
(Cf : continuous_at f (has_Inf.Inf s))
(Af : antitone f)
(ne : s.nonempty)
(H : bdd_below s) :
f (has_Inf.Inf s) = has_Sup.Sup (f '' s)
If an antitone function is continuous at the infimum of a nonempty bounded below set s,
then it sends this infimum to the supremum of the image of s.
theorem
antitone.map_cinfi_of_continuous_at
{α : Type u}
{β : Type v}
{γ : Type w}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_closed_topology β]
[nonempty γ]
{f : α → β}
{g : γ → α}
(Cf : continuous_at f (⨅ (i : γ), g i))
(Af : antitone f)
(H : bdd_below (set.range g)) :
A continuous antitone function sends indexed infimum to indexed supremum in conditionally complete linear order, under a boundedness assumption.
theorem
monotone.tendsto_nhds_within_Iio
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[topological_space α]
[order_topology α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(Mf : monotone f)
(x : α) :
filter.tendsto f (nhds_within x (set.Iio x)) (nhds (has_Sup.Sup (f '' set.Iio x)))
A monotone map has a limit to the left of any point x, equal to Sup (f '' (Iio x)).
theorem
monotone.tendsto_nhds_within_Ioi
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[topological_space α]
[order_topology α]
[conditionally_complete_linear_order β]
[topological_space β]
[order_topology β]
{f : α → β}
(Mf : monotone f)
(x : α) :
filter.tendsto f (nhds_within x (set.Ioi x)) (nhds (has_Inf.Inf (f '' set.Ioi x)))
A monotone map has a limit to the right of any point x, equal to Inf (f '' (Ioi x)).
theorem
eventually_nhds_within_pos_mem_Ioo
{α : Type u}
[linear_order α]
[has_zero α]
[topological_space α]
[order_topology α]
{ε : α}
(h : 0 < ε) :
theorem
eventually_nhds_within_pos_mem_Ioc
{α : Type u}
[linear_order α]
[has_zero α]
[topological_space α]
[order_topology α]
{ε : α}
(h : 0 < ε) :