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;
ClosedIciTopology 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 ClosedIciTopology 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

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

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

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

FirstCountableTopology αᵒᵈ

source

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

SecondCountableTopology αᵒᵈ

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

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

ClosedIciTopology αᵒᵈ

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 IsLUB.range_of_tendsto {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : β → α} {a : α} {F : Filter β} [F.NeBot] (hle : ∀ (i : β), f i ≤ a) (hlim : Filter.Tendsto f F (nhds a)) :

IsLUB (Set.range f) 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 iSup_eq_of_forall_le_of_tendsto {α : Type u} {ι : Type u_1} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLattice α] [TopologicalSpace α] [ClosedIicTopology α] {a : α} {f : ι → α} (hle : ∀ (i : ι), f i ≤ a) (hlim : Filter.Tendsto f F (nhds a)) :

⨆ (i : ι), f i = a

source

theorem iUnion_Iic_eq_Iio_of_lt_of_tendsto {α : Type u} {ι : Type u_1} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] {a : α} {f : ι → α} (hlt : ∀ (i : ι), f i < a) (hlim : Filter.Tendsto f F (nhds a)) :

⋃ (i : ι), Set.Iic (f i) = Set.Iio a

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 Filter.Tendsto.eventually_const_lt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) (h : Tendsto f l (nhds v)) :

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

source

theorem Filter.Tendsto.eventually_const_le {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) (h : 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_nhdsLT {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) :

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

source

theorem Ioo_mem_nhdsLT_of_mem {α : 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.nhdsLT {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (h : a ⋖ b) :

nhdsWithin b (Set.Iio b) = ⊥

source

theorem PredOrder.nhdsLT {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} [PredOrder α] :

nhdsWithin a (Set.Iio a) = ⊥

source

theorem PredOrder.nhdsGT_eq_nhdsNE {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [PredOrder α] (a : α) :

nhdsWithin a (Set.Ioi a) = nhdsWithin a {a}ᶜ

source

theorem PredOrder.nhdsGE_eq_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [PredOrder α] (a : α) :

nhdsWithin a (Set.Ici a) = nhds a

source

theorem Ico_mem_nhdsLT_of_mem {α : 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_nhdsLT {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) :

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

source

theorem Ioc_mem_nhdsLT_of_mem {α : 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_nhdsLT {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) :

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

source

theorem Icc_mem_nhdsLT_of_mem {α : 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_nhdsLT {α : 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_nhdsLT {α : 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_nhdsLT {α : 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 CovBy.nhdsLE {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a ⋖ b) :

nhdsWithin b (Set.Iic b) = pure b

source

theorem PredOrder.nhdsLE {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {b : α} [PredOrder α] :

nhdsWithin b (Set.Iic b) = pure b

source

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

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

source

theorem Ioo_mem_nhdsLE_of_mem {α : 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_nhdsLE_of_mem {α : 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_nhdsLE_of_mem {α : 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_nhdsLE_of_mem {α : 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_nhdsLE {α : 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_nhdsLE {α : 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_nhdsLE {α : 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

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

ClosedIicTopology αᵒᵈ

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 IsGLB.range_of_tendsto {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {f : β → α} {a : α} {F : Filter β} [F.NeBot] (hle : ∀ (i : β), a ≤ f i) (hlim : Filter.Tendsto f F (nhds a)) :

IsGLB (Set.range f) 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 iInf_eq_of_forall_le_of_tendsto {α : Type u} {ι : Type u_1} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLattice α] [TopologicalSpace α] [ClosedIciTopology α] {a : α} {f : ι → α} (hle : ∀ (i : ι), a ≤ f i) (hlim : Filter.Tendsto f F (nhds a)) :

⨅ (i : ι), f i = a

source

theorem iUnion_Ici_eq_Ioi_of_lt_of_tendsto {α : Type u} {ι : Type u_1} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIciTopology α] {a : α} {f : ι → α} (hlt : ∀ (i : ι), a < f i) (hlim : Filter.Tendsto f F (nhds a)) :

⋃ (i : ι), Set.Ici (f i) = Set.Ioi a

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 Filter.Tendsto.eventually_lt_const {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u) (h : Tendsto f l (nhds v)) :

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

source

theorem Filter.Tendsto.eventually_le_const {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u) (h : 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_nhdsGT_of_mem {α : 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_nhdsGT {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (H : a < b) :

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

source

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

nhdsWithin a (Set.Ioi a) = ⊥

source

theorem SuccOrder.nhdsGT {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} [SuccOrder α] :

nhdsWithin a (Set.Ioi a) = ⊥

source

theorem SuccOrder.nhdsLT_eq_nhdsNE {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [SuccOrder α] (a : α) :

nhdsWithin a (Set.Iio a) = nhdsWithin a {a}ᶜ

source

theorem SuccOrder.nhdsLE_eq_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [SuccOrder α] (a : α) :

nhdsWithin a (Set.Iic a) = nhds a

source

theorem Ioc_mem_nhdsGT_of_mem {α : 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_nhdsGT {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (H : a < b) :

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

source

theorem Ico_mem_nhdsGT_of_mem {α : 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_nhdsGT {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (H : a < b) :

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

source

theorem Icc_mem_nhdsGT_of_mem {α : 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_nhdsGT {α : 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_nhdsGT {α : 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_nhdsGT {α : 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 CovBy.nhdsGE {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (H : a ⋖ b) :

nhdsWithin a (Set.Ici a) = pure a

source

theorem SuccOrder.nhdsGE {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} [SuccOrder α] :

nhdsWithin a (Set.Ici a) = pure a

source

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

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

source

theorem Ico_mem_nhdsGE_of_mem {α : 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_nhdsGE_of_mem {α : 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_nhdsGE_of_mem {α : 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_nhdsGE_of_mem {α : 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_nhdsGE {α : 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_nhdsGE {α : 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_nhdsGE {α : 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)

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 α

source

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

ClosedIciTopology α

source

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

OrderClosedTopology αᵒᵈ

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_of_frequently {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : ∃ᶠ (x : β) in b, f x ≤ g x) :

a₁ ≤ a₂

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

theorem isClosed_monotoneOn {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [Preorder β] {s : Set β} :

IsClosed {f : β → α | MonotoneOn f s}

The set of monotone functions on a set is closed.

source

theorem isClosed_monotone {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [Preorder β] :

IsClosed {f : β → α | Monotone f}

The set of monotone functions is closed.

source

theorem isClosed_antitoneOn {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [Preorder β] {s : Set β} :

IsClosed {f : β → α | AntitoneOn f s}

The set of antitone functions on a set is closed.

source

theorem isClosed_antitone {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [Preorder β] :

IsClosed {f : β → α | Antitone f}

The set of antitone functions is closed.

source

@[instance 90]

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

T2Space α

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 DiscreteTopology.of_predOrder_succOrder {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [PredOrder α] [SuccOrder α] :

DiscreteTopology α

The only order closed topology on a linear order which is a PredOrder and a SuccOrder is the discrete topology.

This theorem is not an instance, because it causes searches for PredOrder and SuccOrder with their Preorder arguments and very rarely matches.

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 : Tendsto f l (nhds y)) (hg : 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 : β) => min (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 : β) => max (f b) (g b)

source

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

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

source

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

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

source

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

Tendsto (fun (b : β) => max (f b) (g b)) b (nhds (max a₁ a₂))

source

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

Tendsto (fun (b : β) => min (f b) (g b)) b (nhds (min a₁ a₂))

source

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

Tendsto (fun (i : β) => max a (f i)) l (nhds a)

source

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

Tendsto (fun (i : β) => max (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 : Tendsto f l (nhdsWithin a (Set.Ioi a))) :

Tendsto (fun (i : β) => max 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 : Tendsto f l (nhdsWithin a (Set.Ioi a))) :

Tendsto (fun (i : β) => max (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 : Tendsto f l (nhds a)) :

Tendsto (fun (i : β) => min a (f i)) l (nhds a)

source

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

Tendsto (fun (i : β) => min (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 : Tendsto f l (nhdsWithin a (Set.Iio a))) :

Tendsto (fun (i : β) => min 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 : Tendsto f l (nhdsWithin a (Set.Iio a))) :

Tendsto (fun (i : β) => min (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 (α × β)

source

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

OrderClosedTopology ((i : ι) → α i)

source

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

OrderClosedTopology (α → β)

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` #