Order-closed topologies #

In this file we introduce 3 typeclass mixins that relate topology and order structures:

ClosedIicTopology says that all the intervals $(-∞, a]$ (formally, Set.Iic a) are closed sets;
ClosedIciTopoplogy says that all the intervals $[a, +∞)$ (formally, Set.Ici a) are closed sets;
OrderClosedTopology says that the set of points (x, y) such that x ≤ y is closed in the product topology.

The last predicate implies the first two.

We prove many basic properties of such topologies.

Main statements #

This file contains the proofs of the following facts. For exact requirements (OrderClosedTopology vs ClosedIciTopoplogy vs ClosedIicTopology, PreordervsPartialOrdervsLinearOrder` etc) see their statements.

Open / closed sets #

isOpen_lt : if f and g are continuous functions, then {x | f x < g x} is open;
isOpen_Iio, isOpen_Ioi, isOpen_Ioo : open intervals are open;
isClosed_le : if f and g are continuous functions, then {x | f x ≤ g x} is closed;
isClosed_Iic, isClosed_Ici, isClosed_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};

Convergence and inequalities #

le_of_tendsto_of_tendsto : if f converges to a, g converges to b, and eventually f x ≤ g x, then a ≤ b
le_of_tendsto, ge_of_tendsto : if f converges to a and eventually f x ≤ b (resp., b ≤ f x), then a ≤ b (resp., b ≤ a); we also provide primed versions that assume the inequalities to hold for all x.

Min, max, `sSup` and `sInf` #

Continuous.min, Continuous.max: pointwise min/max of two continuous functions is continuous.
Tendsto.min, Tendsto.max : if f tends to a and g tends to b, then their pointwise min/max tend to min a b and max a b, respectively.

source

class ClosedIicTopology (α : Type u_1) [TopologicalSpace α] [Preorder α] :

Prop

If α is a topological space and a preorder, ClosedIicTopology α means that Iic a is closed for all a : α.

isClosed_Iic : ∀ (a : α), IsClosed (Set.Iic a)
For any a, the set (-∞, a] is closed.

Instances

source

theorem ClosedIicTopology.isClosed_Iic {α : Type u_1} :

∀ {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : ClosedIicTopology α] (a : α), IsClosed (Set.Iic a)

For any a, the set (-∞, a] is closed.

source

class ClosedIciTopology (α : Type u_1) [TopologicalSpace α] [Preorder α] :

Prop

If α is a topological space and a preorder, ClosedIciTopology α means that Ici a is closed for all a : α.

isClosed_Ici : ∀ (a : α), IsClosed (Set.Ici a)
For any a, the set [a, +∞) is closed.

Instances

source

theorem ClosedIciTopology.isClosed_Ici {α : Type u_1} :

∀ {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : ClosedIciTopology α] (a : α), IsClosed (Set.Ici a)

For any a, the set [a, +∞) is closed.

source

class OrderClosedTopology (α : Type u_1) [TopologicalSpace α] [Preorder α] :

Prop

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

isClosed_le' : IsClosed {p : α × α | p.1 ≤ p.2}
The set { (x, y) | x ≤ y } is a closed set.

Instances

source

theorem OrderClosedTopology.isClosed_le' {α : Type u_1} :

∀ {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : OrderClosedTopology α], IsClosed {p : α × α | p.1 ≤ p.2}

The set { (x, y) | x ≤ y } is a closed set.

source

instance instFirstCountableTopologyOrderDual {α : Type u} [TopologicalSpace α] [h : FirstCountableTopology α] :

FirstCountableTopology αᵒᵈ

Equations

⋯ = h

source

instance instSecondCountableTopologyOrderDual {α : Type u} [TopologicalSpace α] [h : SecondCountableTopology α] :

SecondCountableTopology αᵒᵈ

Equations

⋯ = h

source

theorem Dense.orderDual {α : Type u} [TopologicalSpace α] {s : Set α} (hs : Dense s) :

Dense (⇑OrderDual.ofDual ⁻¹' s)

source

theorem BddAbove.of_closure {α : Type u} [TopologicalSpace α] [Preorder α] {s : Set α} :

BddAbove (closure s) → BddAbove s

source

theorem BddBelow.of_closure {α : Type u} [TopologicalSpace α] [Preorder α] {s : Set α} :

BddBelow (closure s) → BddBelow s

source

theorem isClosed_Iic {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {a : α} :

IsClosed (Set.Iic a)

source

@[deprecated ClosedIicTopology.isClosed_Iic]

theorem ClosedIicTopology.isClosed_le' {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] (a : α) :

IsClosed {x : α | x ≤ a}

source

instance instClosedIciTopologyOrderDual {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] :

ClosedIciTopology αᵒᵈ

Equations

⋯ = ⋯

source

@[simp]

theorem closure_Iic {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] (a : α) :

closure (Set.Iic a) = Set.Iic a

source

theorem le_of_tendsto_of_frequently {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : β → α} {a : α} {b : α} {x : Filter β} (lim : Filter.Tendsto f x (nhds a)) (h : ∃ᶠ (c : β) in x, f c ≤ b) :

a ≤ b

source

theorem le_of_tendsto {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : β → α} {a : α} {b : α} {x : Filter β} [x.NeBot] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ᶠ (c : β) in x, f c ≤ b) :

a ≤ b

source

theorem le_of_tendsto' {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : β → α} {a : α} {b : α} {x : Filter β} [x.NeBot] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ (c : β), f c ≤ b) :

a ≤ b

source

@[simp]

theorem upperBounds_closure {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] (s : Set α) :

upperBounds (closure s) = upperBounds s

source

@[simp]

theorem bddAbove_closure {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s : Set α} :

BddAbove (closure s) ↔ BddAbove s

source

theorem BddAbove.closure {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s : Set α} :

BddAbove s → BddAbove (closure s)

Alias of the reverse direction of bddAbove_closure.

source

@[simp]

theorem disjoint_nhds_atBot_iff {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {a : α} :

Disjoint (nhds a) Filter.atBot ↔ ¬IsBot a

source

theorem disjoint_nhds_atBot {α : Type u} [Preorder α] [NoBotOrder α] [TopologicalSpace α] [ClosedIicTopology α] (a : α) :

Disjoint (nhds a) Filter.atBot

source

@[simp]

theorem inf_nhds_atBot {α : Type u} [Preorder α] [NoBotOrder α] [TopologicalSpace α] [ClosedIicTopology α] (a : α) :

nhds a ⊓ Filter.atBot = ⊥

source

theorem not_tendsto_nhds_of_tendsto_atBot {α : Type u} {β : Type v} [Preorder α] [NoBotOrder α] [TopologicalSpace α] [ClosedIicTopology α] {l : Filter β} [l.NeBot] {f : β → α} (hf : Filter.Tendsto f l Filter.atBot) (a : α) :

¬Filter.Tendsto f l (nhds a)

source

theorem not_tendsto_atBot_of_tendsto_nhds {α : Type u} {β : Type v} [Preorder α] [NoBotOrder α] [TopologicalSpace α] [ClosedIicTopology α] {a : α} {l : Filter β} [l.NeBot] {f : β → α} (hf : Filter.Tendsto f l (nhds a)) :

¬Filter.Tendsto f l Filter.atBot

source

theorem isOpen_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} :

IsOpen (Set.Ioi a)

source

@[simp]

theorem interior_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} :

interior (Set.Ioi a) = Set.Ioi a

source

theorem Ioi_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (h : a < b) :

Set.Ioi a ∈ nhds b

source

theorem eventually_gt_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (hab : b < a) :

∀ᶠ (x : α) in nhds a, b < x

source

theorem Ici_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (h : a < b) :

Set.Ici a ∈ nhds b

source

theorem eventually_ge_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (hab : b < a) :

∀ᶠ (x : α) in nhds a, b ≤ x

source

theorem eventually_gt_of_tendsto_gt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {l : Filter γ} {f : γ → α} {u : α} {v : α} (hv : u < v) (h : Filter.Tendsto f l (nhds v)) :

∀ᶠ (a : γ) in l, u < f a

source

theorem eventually_ge_of_tendsto_gt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {l : Filter γ} {f : γ → α} {u : α} {v : α} (hv : u < v) (h : Filter.Tendsto f l (nhds v)) :

∀ᶠ (a : γ) in l, u ≤ f a

source

theorem Dense.exists_gt {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) :

∃ y ∈ s, x < y

source

theorem Dense.exists_ge {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) :

∃ y ∈ s, x ≤ y

source

theorem Dense.exists_ge' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {s : Set α} (hs : Dense s) (htop : ∀ (x : α), IsTop x → x ∈ s) (x : α) :

∃ y ∈ s, x ≤ y

Left neighborhoods on a `ClosedIicTopology` #

Limits to the left of real functions are defined in terms of neighborhoods to the left, either open or closed, i.e., members of 𝓝[<] a and 𝓝[≤] a. Here we prove that all left-neighborhoods of a point are equal, and we prove other useful characterizations which require the stronger hypothesis OrderTopology α in another file.

Point excluded #

source

theorem Ioo_mem_nhdsWithin_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (H : a < b) :

Set.Ioo a b ∈ nhdsWithin b (Set.Iio b)

source

theorem Ioo_mem_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ioc a c) :

Set.Ioo a c ∈ nhdsWithin b (Set.Iio b)

source

theorem CovBy.nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (h : a ⋖ b) :

nhdsWithin b (Set.Iio b) = ⊥

source

theorem Ico_mem_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ioc a c) :

Set.Ico a c ∈ nhdsWithin b (Set.Iio b)

source

theorem Ico_mem_nhdsWithin_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (H : a < b) :

Set.Ico a b ∈ nhdsWithin b (Set.Iio b)

source

theorem Ioc_mem_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ioc a c) :

Set.Ioc a c ∈ nhdsWithin b (Set.Iio b)

source

theorem Ioc_mem_nhdsWithin_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (H : a < b) :

Set.Ioc a b ∈ nhdsWithin b (Set.Iio b)

source

theorem Icc_mem_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ioc a c) :

Set.Icc a c ∈ nhdsWithin b (Set.Iio b)

source

theorem Icc_mem_nhdsWithin_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (H : a < b) :

Set.Icc a b ∈ nhdsWithin b (Set.Iio b)

source

@[simp]

theorem nhdsWithin_Ico_eq_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (h : a < b) :

nhdsWithin b (Set.Ico a b) = nhdsWithin b (Set.Iio b)

source

@[simp]

theorem nhdsWithin_Ioo_eq_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (h : a < b) :

nhdsWithin b (Set.Ioo a b) = nhdsWithin b (Set.Iio b)

source

@[simp]

theorem continuousWithinAt_Ico_iff_Iio {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [TopologicalSpace β] {a : α} {b : α} {f : α → β} (h : a < b) :

ContinuousWithinAt f (Set.Ico a b) b ↔ ContinuousWithinAt f (Set.Iio b) b

source

@[simp]

theorem continuousWithinAt_Ioo_iff_Iio {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [TopologicalSpace β] {a : α} {b : α} {f : α → β} (h : a < b) :

ContinuousWithinAt f (Set.Ioo a b) b ↔ ContinuousWithinAt f (Set.Iio b) b

Point included #

source

theorem Ioc_mem_nhdsWithin_Iic' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (H : a < b) :

Set.Ioc a b ∈ nhdsWithin b (Set.Iic b)

source

theorem Ioo_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ioo a c) :

Set.Ioo a c ∈ nhdsWithin b (Set.Iic b)

source

theorem Ico_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ioo a c) :

Set.Ico a c ∈ nhdsWithin b (Set.Iic b)

source

theorem Ioc_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ioc a c) :

Set.Ioc a c ∈ nhdsWithin b (Set.Iic b)

source

theorem Icc_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ioc a c) :

Set.Icc a c ∈ nhdsWithin b (Set.Iic b)

source

theorem Icc_mem_nhdsWithin_Iic' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (H : a < b) :

Set.Icc a b ∈ nhdsWithin b (Set.Iic b)

source

@[simp]

theorem nhdsWithin_Icc_eq_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (h : a < b) :

nhdsWithin b (Set.Icc a b) = nhdsWithin b (Set.Iic b)

source

@[simp]

theorem nhdsWithin_Ioc_eq_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} {b : α} (h : a < b) :

nhdsWithin b (Set.Ioc a b) = nhdsWithin b (Set.Iic b)

source

@[simp]

theorem continuousWithinAt_Icc_iff_Iic {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [TopologicalSpace β] {a : α} {b : α} {f : α → β} (h : a < b) :

ContinuousWithinAt f (Set.Icc a b) b ↔ ContinuousWithinAt f (Set.Iic b) b

source

@[simp]

theorem continuousWithinAt_Ioc_iff_Iic {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [TopologicalSpace β] {a : α} {b : α} {f : α → β} (h : a < b) :

ContinuousWithinAt f (Set.Ioc a b) b ↔ ContinuousWithinAt f (Set.Iic b) b

source

theorem isClosed_Ici {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {a : α} :

IsClosed (Set.Ici a)

source

@[deprecated]

theorem ClosedIciTopology.isClosed_ge' {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] (a : α) :

IsClosed {x : α | a ≤ x}

source

instance instClosedIicTopologyOrderDual {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] :

ClosedIicTopology αᵒᵈ

Equations

⋯ = ⋯

source

@[simp]

theorem closure_Ici {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] (a : α) :

closure (Set.Ici a) = Set.Ici a

source

theorem ge_of_tendsto_of_frequently {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {f : β → α} {a : α} {b : α} {x : Filter β} (lim : Filter.Tendsto f x (nhds a)) (h : ∃ᶠ (c : β) in x, b ≤ f c) :

b ≤ a

source

theorem ge_of_tendsto {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {f : β → α} {a : α} {b : α} {x : Filter β} [x.NeBot] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ᶠ (c : β) in x, b ≤ f c) :

b ≤ a

source

theorem ge_of_tendsto' {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {f : β → α} {a : α} {b : α} {x : Filter β} [x.NeBot] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ (c : β), b ≤ f c) :

b ≤ a

source

@[simp]

theorem lowerBounds_closure {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] (s : Set α) :

lowerBounds (closure s) = lowerBounds s

source

@[simp]

theorem bddBelow_closure {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {s : Set α} :

BddBelow (closure s) ↔ BddBelow s

source

theorem BddBelow.closure {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {s : Set α} :

BddBelow s → BddBelow (closure s)

Alias of the reverse direction of bddBelow_closure.

source

@[simp]

theorem disjoint_nhds_atTop_iff {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {a : α} :

Disjoint (nhds a) Filter.atTop ↔ ¬IsTop a

source

theorem disjoint_nhds_atTop {α : Type u} [Preorder α] [NoTopOrder α] [TopologicalSpace α] [ClosedIciTopology α] (a : α) :

Disjoint (nhds a) Filter.atTop

source

@[simp]

theorem inf_nhds_atTop {α : Type u} [Preorder α] [NoTopOrder α] [TopologicalSpace α] [ClosedIciTopology α] (a : α) :

nhds a ⊓ Filter.atTop = ⊥

source

theorem not_tendsto_nhds_of_tendsto_atTop {α : Type u} {β : Type v} [Preorder α] [NoTopOrder α] [TopologicalSpace α] [ClosedIciTopology α] {l : Filter β} [l.NeBot] {f : β → α} (hf : Filter.Tendsto f l Filter.atTop) (a : α) :

¬Filter.Tendsto f l (nhds a)

source

theorem not_tendsto_atTop_of_tendsto_nhds {α : Type u} {β : Type v} [Preorder α] [NoTopOrder α] [TopologicalSpace α] [ClosedIciTopology α] {a : α} {l : Filter β} [l.NeBot] {f : β → α} (hf : Filter.Tendsto f l (nhds a)) :

¬Filter.Tendsto f l Filter.atTop

source

theorem isOpen_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} :

IsOpen (Set.Iio a)

source

@[simp]

theorem interior_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} :

interior (Set.Iio a) = Set.Iio a

source

theorem Iio_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (h : a < b) :

Set.Iio b ∈ nhds a

source

theorem eventually_lt_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (hab : a < b) :

∀ᶠ (x : α) in nhds a, x < b

source

theorem Iic_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (h : a < b) :

Set.Iic b ∈ nhds a

source

theorem eventually_le_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (hab : a < b) :

∀ᶠ (x : α) in nhds a, x ≤ b

source

theorem eventually_lt_of_tendsto_lt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {l : Filter γ} {f : γ → α} {u : α} {v : α} (hv : v < u) (h : Filter.Tendsto f l (nhds v)) :

∀ᶠ (a : γ) in l, f a < u

source

theorem eventually_le_of_tendsto_lt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {l : Filter γ} {f : γ → α} {u : α} {v : α} (hv : v < u) (h : Filter.Tendsto f l (nhds v)) :

∀ᶠ (a : γ) in l, f a ≤ u

source

theorem Dense.exists_lt {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) :

∃ y ∈ s, y < x

source

theorem Dense.exists_le {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) :

∃ y ∈ s, y ≤ x

source

theorem Dense.exists_le' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {s : Set α} (hs : Dense s) (hbot : ∀ (x : α), IsBot x → x ∈ s) (x : α) :

∃ y ∈ s, y ≤ x

Right neighborhoods on a `ClosedIciTopology` #

Limits to the right of real functions are defined in terms of neighborhoods to the right, either open or closed, i.e., members of 𝓝[>] a and 𝓝[≥] a. Here we prove that all right-neighborhoods of a point are equal, and we prove other useful characterizations which require the stronger hypothesis OrderTopology α in another file.

Point excluded #

source

theorem Ioo_mem_nhdsWithin_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ico a c) :

Set.Ioo a c ∈ nhdsWithin b (Set.Ioi b)

source

theorem Ioo_mem_nhdsWithin_Ioi' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (H : a < b) :

Set.Ioo a b ∈ nhdsWithin a (Set.Ioi a)

source

theorem CovBy.nhdsWithin_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (h : a ⋖ b) :

nhdsWithin a (Set.Ioi a) = ⊥

source

theorem Ioc_mem_nhdsWithin_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ico a c) :

Set.Ioc a c ∈ nhdsWithin b (Set.Ioi b)

source

theorem Ioc_mem_nhdsWithin_Ioi' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (H : a < b) :

Set.Ioc a b ∈ nhdsWithin a (Set.Ioi a)

source

theorem Ico_mem_nhdsWithin_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ico a c) :

Set.Ico a c ∈ nhdsWithin b (Set.Ioi b)

source

theorem Ico_mem_nhdsWithin_Ioi' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (H : a < b) :

Set.Ico a b ∈ nhdsWithin a (Set.Ioi a)

source

theorem Icc_mem_nhdsWithin_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ico a c) :

Set.Icc a c ∈ nhdsWithin b (Set.Ioi b)

source

theorem Icc_mem_nhdsWithin_Ioi' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (H : a < b) :

Set.Icc a b ∈ nhdsWithin a (Set.Ioi a)

source

@[simp]

theorem nhdsWithin_Ioc_eq_nhdsWithin_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (h : a < b) :

nhdsWithin a (Set.Ioc a b) = nhdsWithin a (Set.Ioi a)

source

@[simp]

theorem nhdsWithin_Ioo_eq_nhdsWithin_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (h : a < b) :

nhdsWithin a (Set.Ioo a b) = nhdsWithin a (Set.Ioi a)

source

@[simp]

theorem continuousWithinAt_Ioc_iff_Ioi {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [TopologicalSpace β] {a : α} {b : α} {f : α → β} (h : a < b) :

ContinuousWithinAt f (Set.Ioc a b) a ↔ ContinuousWithinAt f (Set.Ioi a) a

source

@[simp]

theorem continuousWithinAt_Ioo_iff_Ioi {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [TopologicalSpace β] {a : α} {b : α} {f : α → β} (h : a < b) :

ContinuousWithinAt f (Set.Ioo a b) a ↔ ContinuousWithinAt f (Set.Ioi a) a

Point included #

source

theorem Ico_mem_nhdsWithin_Ici' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (H : a < b) :

Set.Ico a b ∈ nhdsWithin a (Set.Ici a)

source

theorem Ico_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ico a c) :

Set.Ico a c ∈ nhdsWithin b (Set.Ici b)

source

theorem Ioo_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ioo a c) :

Set.Ioo a c ∈ nhdsWithin b (Set.Ici b)

source

theorem Ioc_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ioo a c) :

Set.Ioc a c ∈ nhdsWithin b (Set.Ici b)

source

theorem Icc_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} {c : α} (H : b ∈ Set.Ico a c) :

Set.Icc a c ∈ nhdsWithin b (Set.Ici b)

source

theorem Icc_mem_nhdsWithin_Ici' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (H : a < b) :

Set.Icc a b ∈ nhdsWithin a (Set.Ici a)

source

@[simp]

theorem nhdsWithin_Icc_eq_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (h : a < b) :

nhdsWithin a (Set.Icc a b) = nhdsWithin a (Set.Ici a)

source

@[simp]

theorem nhdsWithin_Ico_eq_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} {b : α} (h : a < b) :

nhdsWithin a (Set.Ico a b) = nhdsWithin a (Set.Ici a)

source

@[simp]

theorem continuousWithinAt_Icc_iff_Ici {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [TopologicalSpace β] {a : α} {b : α} {f : α → β} (h : a < b) :

ContinuousWithinAt f (Set.Icc a b) a ↔ ContinuousWithinAt f (Set.Ici a) a

source

@[simp]

theorem continuousWithinAt_Ico_iff_Ici {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [TopologicalSpace β] {a : α} {b : α} {f : α → β} (h : a < b) :

ContinuousWithinAt f (Set.Ico a b) a ↔ ContinuousWithinAt f (Set.Ici a) a

source

instance Subtype.instOrderClosedTopology {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {p : α → Prop} :

OrderClosedTopology (Subtype p)

Equations

⋯ = ⋯

source

theorem isClosed_le_prod {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] :

IsClosed {p : α × α | p.1 ≤ p.2}

source

theorem isClosed_le {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f : β → α} {g : β → α} (hf : Continuous f) (hg : Continuous g) :

IsClosed {b : β | f b ≤ g b}

source

instance instClosedIicTopology {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] :

ClosedIicTopology α

Equations

⋯ = ⋯

source

instance instClosedIciTopology {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] :

ClosedIciTopology α

Equations

⋯ = ⋯

source

instance instOrderClosedTopologyOrderDual {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] :

OrderClosedTopology αᵒᵈ

Equations

⋯ = ⋯

source

theorem isClosed_Icc {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {a : α} {b : α} :

IsClosed (Set.Icc a b)

source

@[simp]

theorem closure_Icc {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] (a : α) (b : α) :

closure (Set.Icc a b) = Set.Icc a b

source

theorem le_of_tendsto_of_tendsto {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f : β → α} {g : β → α} {b : Filter β} {a₁ : α} {a₂ : α} [b.NeBot] (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : f ≤ᶠ[b] g) :

a₁ ≤ a₂

source

theorem tendsto_le_of_eventuallyLE {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f : β → α} {g : β → α} {b : Filter β} {a₁ : α} {a₂ : α} [b.NeBot] (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.

source

theorem le_of_tendsto_of_tendsto' {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f : β → α} {g : β → α} {b : Filter β} {a₁ : α} {a₂ : α} [b.NeBot] (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : ∀ (x : β), f x ≤ g x) :

a₁ ≤ a₂

source

@[simp]

theorem closure_le_eq {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f : β → α} {g : β → α} (hf : Continuous f) (hg : Continuous g) :

closure {b : β | f b ≤ g b} = {b : β | f b ≤ g b}

source

theorem closure_lt_subset_le {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f : β → α} {g : β → α} (hf : Continuous f) (hg : Continuous g) :

closure {b : β | f b < g b} ⊆ {b : β | f b ≤ g b}

source

theorem ContinuousWithinAt.closure_le {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f : β → α} {g : β → α} {s : Set β} {x : β} (hx : x ∈ closure s) (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) (h : ∀ y ∈ s, f y ≤ g y) :

f x ≤ g x

source

theorem IsClosed.isClosed_le {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f : β → α} {g : β → α} {s : Set β} (hs : IsClosed s) (hf : ContinuousOn f s) (hg : ContinuousOn g s) :

IsClosed {x : β | x ∈ s ∧ f x ≤ g x}

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

source

theorem le_on_closure {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f : β → α} {g : β → α} {s : Set β} (h : ∀ x ∈ s, f x ≤ g x) (hf : ContinuousOn f (closure s)) (hg : ContinuousOn g (closure s)) ⦃x : β⦄ (hx : x ∈ closure s) :

f x ≤ g x

source

theorem IsClosed.epigraph {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f : β → α} {s : Set β} (hs : IsClosed s) (hf : ContinuousOn f s) :

IsClosed {p : β × α | p.1 ∈ s ∧ f p.1 ≤ p.2}

source

theorem IsClosed.hypograph {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f : β → α} {s : Set β} (hs : IsClosed s) (hf : ContinuousOn f s) :

IsClosed {p : β × α | p.1 ∈ s ∧ p.2 ≤ f p.1}

source

@[instance 90]

instance OrderClosedTopology.to_t2Space {α : Type u} [TopologicalSpace α] [PartialOrder α] [t : OrderClosedTopology α] :

T2Space α

Equations

⋯ = ⋯

source

theorem isOpen_lt {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [TopologicalSpace β] {f : β → α} {g : β → α} (hf : Continuous f) (hg : Continuous g) :

IsOpen {b : β | f b < g b}

source

theorem isOpen_lt_prod {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] :

IsOpen {p : α × α | p.1 < p.2}

source

theorem isOpen_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} :

IsOpen (Set.Ioo a b)

source

@[simp]

theorem interior_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} :

interior (Set.Ioo a b) = Set.Ioo a b

source

theorem Ioo_subset_closure_interior {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} :

Set.Ioo a b ⊆ closure (interior (Set.Ioo a b))

source

theorem Ioo_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {x : α} (ha : a < x) (hb : x < b) :

Set.Ioo a b ∈ nhds x

source

theorem Ioc_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {x : α} (ha : a < x) (hb : x < b) :

Set.Ioc a b ∈ nhds x

source

theorem Ico_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {x : α} (ha : a < x) (hb : x < b) :

Set.Ico a b ∈ nhds x

source

theorem Icc_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {x : α} (ha : a < x) (hb : x < b) :

Set.Icc a b ∈ nhds x

source

theorem lt_subset_interior_le {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {g : β → α} [TopologicalSpace β] (hf : Continuous f) (hg : Continuous g) :

{b : β | f b < g b} ⊆ interior {b : β | f b ≤ g b}

source

theorem frontier_le_subset_eq {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {g : β → α} [TopologicalSpace β] (hf : Continuous f) (hg : Continuous g) :

frontier {b : β | f b ≤ g b} ⊆ {b : β | f b = g b}

source

theorem frontier_Iic_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] (a : α) :

frontier (Set.Iic a) ⊆ {a}

source

theorem frontier_Ici_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] (a : α) :

frontier (Set.Ici a) ⊆ {a}

source

theorem frontier_lt_subset_eq {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {g : β → α} [TopologicalSpace β] (hf : Continuous f) (hg : Continuous g) :

frontier {b : β | f b < g b} ⊆ {b : β | f b = g b}

source

theorem continuous_if_le {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {g : β → α} [TopologicalSpace β] [TopologicalSpace γ] [(x : β) → Decidable (f x ≤ g x)] {f' : β → γ} {g' : β → γ} (hf : Continuous f) (hg : Continuous g) (hf' : ContinuousOn f' {x : β | f x ≤ g x}) (hg' : ContinuousOn g' {x : β | g x ≤ f x}) (hfg : ∀ (x : β), f x = g x → f' x = g' x) :

Continuous fun (x : β) => if f x ≤ g x then f' x else g' x

source

theorem Continuous.if_le {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {g : β → α} [TopologicalSpace β] [TopologicalSpace γ] [(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 fun (x : β) => if f x ≤ g x then f' x else g' x

source

theorem Filter.Tendsto.eventually_lt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {l : Filter γ} {f : γ → α} {g : γ → α} {y : α} {z : α} (hf : Filter.Tendsto f l (nhds y)) (hg : Filter.Tendsto g l (nhds z)) (hyz : y < z) :

∀ᶠ (x : γ) in l, f x < g x

source

theorem ContinuousAt.eventually_lt {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {g : β → α} [TopologicalSpace β] {x₀ : β} (hf : ContinuousAt f x₀) (hg : ContinuousAt g x₀) (hfg : f x₀ < g x₀) :

∀ᶠ (x : β) in nhds x₀, f x < g x

source

theorem Continuous.min {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {g : β → α} [TopologicalSpace β] (hf : Continuous f) (hg : Continuous g) :

Continuous fun (b : β) => f b ⊓ g b

source

theorem Continuous.max {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {g : β → α} [TopologicalSpace β] (hf : Continuous f) (hg : Continuous g) :

Continuous fun (b : β) => f b ⊔ g b

source

theorem continuous_min {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] :

Continuous fun (p : α × α) => p.1 ⊓ p.2

source

theorem continuous_max {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] :

Continuous fun (p : α × α) => p.1 ⊔ p.2

source

theorem Filter.Tendsto.max {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {g : β → α} {b : Filter β} {a₁ : α} {a₂ : α} (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) :

Filter.Tendsto (fun (b : β) => f b ⊔ g b) b (nhds (a₁ ⊔ a₂))

source

theorem Filter.Tendsto.min {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {g : β → α} {b : Filter β} {a₁ : α} {a₂ : α} (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) :

Filter.Tendsto (fun (b : β) => f b ⊓ g b) b (nhds (a₁ ⊓ a₂))

source

theorem Filter.Tendsto.max_right {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhds a)) :

Filter.Tendsto (fun (i : β) => a ⊔ f i) l (nhds a)

source

theorem Filter.Tendsto.max_left {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhds a)) :

Filter.Tendsto (fun (i : β) => f i ⊔ a) l (nhds a)

source

theorem Filter.tendsto_nhds_max_right {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhdsWithin a (Set.Ioi a))) :

Filter.Tendsto (fun (i : β) => a ⊔ f i) l (nhdsWithin a (Set.Ioi a))

source

theorem Filter.tendsto_nhds_max_left {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhdsWithin a (Set.Ioi a))) :

Filter.Tendsto (fun (i : β) => f i ⊔ a) l (nhdsWithin a (Set.Ioi a))

source

theorem Filter.Tendsto.min_right {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhds a)) :

Filter.Tendsto (fun (i : β) => a ⊓ f i) l (nhds a)

source

theorem Filter.Tendsto.min_left {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhds a)) :

Filter.Tendsto (fun (i : β) => f i ⊓ a) l (nhds a)

source

theorem Filter.tendsto_nhds_min_right {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhdsWithin a (Set.Iio a))) :

Filter.Tendsto (fun (i : β) => a ⊓ f i) l (nhdsWithin a (Set.Iio a))

source

theorem Filter.tendsto_nhds_min_left {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhdsWithin a (Set.Iio a))) :

Filter.Tendsto (fun (i : β) => f i ⊓ a) l (nhdsWithin a (Set.Iio a))

source

theorem Dense.exists_between {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) {x : α} {y : α} (h : x < y) :

∃ z ∈ s, z ∈ Set.Ioo x y

source

theorem Dense.Ioi_eq_biUnion {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) :

Set.Ioi x = ⋃ y ∈ s ∩ Set.Ioi x, Set.Ioi y

source

theorem Dense.Iio_eq_biUnion {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) :

Set.Iio x = ⋃ y ∈ s ∩ Set.Iio x, Set.Iio y

source

instance instOrderClosedTopologyProd {α : Type u} {β : Type v} [Preorder α] [TopologicalSpace α] [OrderClosedTopology α] [Preorder β] [TopologicalSpace β] [OrderClosedTopology β] :

OrderClosedTopology (α × β)

Equations

⋯ = ⋯

source

instance instOrderClosedTopologyForall {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OrderClosedTopology (α i)] :

OrderClosedTopology ((i : ι) → α i)

Equations

⋯ = ⋯

source

instance Pi.orderClosedTopology' {α : Type u} {β : Type v} [Preorder β] [TopologicalSpace β] [OrderClosedTopology β] :

OrderClosedTopology (α → β)

Equations

⋯ = ⋯

Documentation

Mathlib.Topology.Order.OrderClosed

Order-closed topologies #

Main statements #

Open / closed sets #

Convergence and inequalities #

Min, max, `sSup` and `sInf` #

Left neighborhoods on a `ClosedIicTopology` #

Point excluded #

Point included #

Right neighborhoods on a `ClosedIciTopology` #

Point excluded #

Point included #

Order-closed topologies #

Main statements #

Open / closed sets #

Convergence and inequalities #

Min, max, sSup and sInf #

Left neighborhoods on a ClosedIicTopology #

Point excluded #

Point included #

Right neighborhoods on a ClosedIciTopology #

Point excluded #

Point included #

Min, max, `sSup` and `sInf` #

Left neighborhoods on a `ClosedIicTopology` #

Right neighborhoods on a `ClosedIciTopology` #