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.
class ClosedIicTopology (α : Type u_1) [] [] :

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

• isClosed_Iic : ∀ (a : α), IsClosed ()

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

Instances
theorem ClosedIicTopology.isClosed_Iic {α : Type u_1} [] [] [self : ] (a : α) :

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

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

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

• isClosed_Ici : ∀ (a : α), IsClosed ()

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

Instances
theorem ClosedIciTopology.isClosed_Ici {α : Type u_1} [] [] [self : ] (a : α) :

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

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

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
theorem OrderClosedTopology.isClosed_le' {α : Type u_1} [] [] [self : ] :
IsClosed {p : α × α | p.1 p.2}

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

instance instFirstCountableTopologyOrderDual {α : Type u} [] [h : ] :
Equations
• = h
instance instSecondCountableTopologyOrderDual {α : Type u} [] [h : ] :
Equations
• = h
theorem Dense.orderDual {α : Type u} [] {s : Set α} (hs : ) :
Dense (OrderDual.ofDual ⁻¹' s)
theorem BddAbove.of_closure {α : Type u} [] [] {s : Set α} :
BddAbove ()
theorem BddBelow.of_closure {α : Type u} [] [] {s : Set α} :
BddBelow ()
theorem isClosed_Iic {α : Type u} [] [] {a : α} :
@[deprecated ClosedIicTopology.isClosed_Iic]
theorem ClosedIicTopology.isClosed_le' {α : Type u} [] [] (a : α) :
IsClosed {x : α | x a}
instance instClosedIciTopologyOrderDual {α : Type u} [] [] :
Equations
• =
@[simp]
theorem closure_Iic {α : Type u} [] [] (a : α) :
theorem le_of_tendsto_of_frequently {α : Type u} {β : Type v} [] [] {f : βα} {a : α} {b : α} {x : } (lim : Filter.Tendsto f x (nhds a)) (h : ∃ᶠ (c : β) in x, f c b) :
a b
theorem le_of_tendsto {α : Type u} {β : Type v} [] [] {f : βα} {a : α} {b : α} {x : } [x.NeBot] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ᶠ (c : β) in x, f c b) :
a b
theorem le_of_tendsto' {α : Type u} {β : Type v} [] [] {f : βα} {a : α} {b : α} {x : } [x.NeBot] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ (c : β), f c b) :
a b
@[simp]
theorem upperBounds_closure {α : Type u} [] [] (s : Set α) :
@[simp]
theorem bddAbove_closure {α : Type u} [] [] {s : Set α} :
theorem BddAbove.closure {α : Type u} [] [] {s : Set α} :
BddAbove ()

Alias of the reverse direction of bddAbove_closure.

@[simp]
theorem disjoint_nhds_atBot_iff {α : Type u} [] [] {a : α} :
Disjoint (nhds a) Filter.atBot ¬
theorem disjoint_nhds_atBot {α : Type u} [] [] [] (a : α) :
Disjoint (nhds a) Filter.atBot
@[simp]
theorem inf_nhds_atBot {α : Type u} [] [] [] (a : α) :
nhds a Filter.atBot =
theorem not_tendsto_nhds_of_tendsto_atBot {α : Type u} {β : Type v} [] [] [] {l : } [l.NeBot] {f : βα} (hf : Filter.Tendsto f l Filter.atBot) (a : α) :
theorem not_tendsto_atBot_of_tendsto_nhds {α : Type u} {β : Type v} [] [] [] {a : α} {l : } [l.NeBot] {f : βα} (hf : Filter.Tendsto f l (nhds a)) :
¬Filter.Tendsto f l Filter.atBot
theorem isOpen_Ioi {α : Type u} [] [] {a : α} :
@[simp]
theorem interior_Ioi {α : Type u} [] [] {a : α} :
theorem Ioi_mem_nhds {α : Type u} [] [] {a : α} {b : α} (h : a < b) :
theorem eventually_gt_nhds {α : Type u} [] [] {a : α} {b : α} (hab : b < a) :
∀ᶠ (x : α) in nhds a, b < x
theorem Ici_mem_nhds {α : Type u} [] [] {a : α} {b : α} (h : a < b) :
theorem eventually_ge_nhds {α : Type u} [] [] {a : α} {b : α} (hab : b < a) :
∀ᶠ (x : α) in nhds a, b x
theorem eventually_gt_of_tendsto_gt {α : Type u} {γ : Type w} [] [] {l : } {f : γα} {u : α} {v : α} (hv : u < v) (h : Filter.Tendsto f l (nhds v)) :
∀ᶠ (a : γ) in l, u < f a
theorem eventually_ge_of_tendsto_gt {α : Type u} {γ : Type w} [] [] {l : } {f : γα} {u : α} {v : α} (hv : u < v) (h : Filter.Tendsto f l (nhds v)) :
∀ᶠ (a : γ) in l, u f a
theorem Dense.exists_gt {α : Type u} [] [] [] {s : Set α} (hs : ) (x : α) :
ys, x < y
theorem Dense.exists_ge {α : Type u} [] [] [] {s : Set α} (hs : ) (x : α) :
ys, x y
theorem Dense.exists_ge' {α : Type u} [] [] {s : Set α} (hs : ) (htop : ∀ (x : α), x s) (x : α) :
ys, 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 #

theorem Ioo_mem_nhdsWithin_Iio' {α : Type u} [] [] {a : α} {b : α} (H : a < b) :
theorem Ioo_mem_nhdsWithin_Iio {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ioc a c) :
theorem CovBy.nhdsWithin_Iio {α : Type u} [] [] {a : α} {b : α} (h : a b) :
theorem Ico_mem_nhdsWithin_Iio {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ioc a c) :
theorem Ico_mem_nhdsWithin_Iio' {α : Type u} [] [] {a : α} {b : α} (H : a < b) :
theorem Ioc_mem_nhdsWithin_Iio {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ioc a c) :
theorem Ioc_mem_nhdsWithin_Iio' {α : Type u} [] [] {a : α} {b : α} (H : a < b) :
theorem Icc_mem_nhdsWithin_Iio {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ioc a c) :
theorem Icc_mem_nhdsWithin_Iio' {α : Type u} [] [] {a : α} {b : α} (H : a < b) :
@[simp]
theorem nhdsWithin_Ico_eq_nhdsWithin_Iio {α : Type u} [] [] {a : α} {b : α} (h : a < b) :
@[simp]
theorem nhdsWithin_Ioo_eq_nhdsWithin_Iio {α : Type u} [] [] {a : α} {b : α} (h : a < b) :
@[simp]
theorem continuousWithinAt_Ico_iff_Iio {α : Type u} {β : Type v} [] [] [] {a : α} {b : α} {f : αβ} (h : a < b) :
@[simp]
theorem continuousWithinAt_Ioo_iff_Iio {α : Type u} {β : Type v} [] [] [] {a : α} {b : α} {f : αβ} (h : a < b) :

Point included #

theorem Ioc_mem_nhdsWithin_Iic' {α : Type u} [] [] {a : α} {b : α} (H : a < b) :
theorem Ioo_mem_nhdsWithin_Iic {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ioo a c) :
theorem Ico_mem_nhdsWithin_Iic {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ioo a c) :
theorem Ioc_mem_nhdsWithin_Iic {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ioc a c) :
theorem Icc_mem_nhdsWithin_Iic {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ioc a c) :
theorem Icc_mem_nhdsWithin_Iic' {α : Type u} [] [] {a : α} {b : α} (H : a < b) :
@[simp]
theorem nhdsWithin_Icc_eq_nhdsWithin_Iic {α : Type u} [] [] {a : α} {b : α} (h : a < b) :
@[simp]
theorem nhdsWithin_Ioc_eq_nhdsWithin_Iic {α : Type u} [] [] {a : α} {b : α} (h : a < b) :
@[simp]
theorem continuousWithinAt_Icc_iff_Iic {α : Type u} {β : Type v} [] [] [] {a : α} {b : α} {f : αβ} (h : a < b) :
@[simp]
theorem continuousWithinAt_Ioc_iff_Iic {α : Type u} {β : Type v} [] [] [] {a : α} {b : α} {f : αβ} (h : a < b) :
theorem isClosed_Ici {α : Type u} [] [] {a : α} :
@[deprecated]
theorem ClosedIciTopology.isClosed_ge' {α : Type u} [] [] (a : α) :
IsClosed {x : α | a x}
instance instClosedIicTopologyOrderDual {α : Type u} [] [] :
Equations
• =
@[simp]
theorem closure_Ici {α : Type u} [] [] (a : α) :
theorem ge_of_tendsto_of_frequently {α : Type u} {β : Type v} [] [] {f : βα} {a : α} {b : α} {x : } (lim : Filter.Tendsto f x (nhds a)) (h : ∃ᶠ (c : β) in x, b f c) :
b a
theorem ge_of_tendsto {α : Type u} {β : Type v} [] [] {f : βα} {a : α} {b : α} {x : } [x.NeBot] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ᶠ (c : β) in x, b f c) :
b a
theorem ge_of_tendsto' {α : Type u} {β : Type v} [] [] {f : βα} {a : α} {b : α} {x : } [x.NeBot] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ (c : β), b f c) :
b a
@[simp]
theorem lowerBounds_closure {α : Type u} [] [] (s : Set α) :
@[simp]
theorem bddBelow_closure {α : Type u} [] [] {s : Set α} :
theorem BddBelow.closure {α : Type u} [] [] {s : Set α} :
BddBelow ()

Alias of the reverse direction of bddBelow_closure.

@[simp]
theorem disjoint_nhds_atTop_iff {α : Type u} [] [] {a : α} :
Disjoint (nhds a) Filter.atTop ¬
theorem disjoint_nhds_atTop {α : Type u} [] [] [] (a : α) :
Disjoint (nhds a) Filter.atTop
@[simp]
theorem inf_nhds_atTop {α : Type u} [] [] [] (a : α) :
nhds a Filter.atTop =
theorem not_tendsto_nhds_of_tendsto_atTop {α : Type u} {β : Type v} [] [] [] {l : } [l.NeBot] {f : βα} (hf : Filter.Tendsto f l Filter.atTop) (a : α) :
theorem not_tendsto_atTop_of_tendsto_nhds {α : Type u} {β : Type v} [] [] [] {a : α} {l : } [l.NeBot] {f : βα} (hf : Filter.Tendsto f l (nhds a)) :
¬Filter.Tendsto f l Filter.atTop
theorem isOpen_Iio {α : Type u} [] [] {a : α} :
@[simp]
theorem interior_Iio {α : Type u} [] [] {a : α} :
theorem Iio_mem_nhds {α : Type u} [] [] {a : α} {b : α} (h : a < b) :
theorem eventually_lt_nhds {α : Type u} [] [] {a : α} {b : α} (hab : a < b) :
∀ᶠ (x : α) in nhds a, x < b
theorem Iic_mem_nhds {α : Type u} [] [] {a : α} {b : α} (h : a < b) :
theorem eventually_le_nhds {α : Type u} [] [] {a : α} {b : α} (hab : a < b) :
∀ᶠ (x : α) in nhds a, x b
theorem eventually_lt_of_tendsto_lt {α : Type u} {γ : Type w} [] [] {l : } {f : γα} {u : α} {v : α} (hv : v < u) (h : Filter.Tendsto f l (nhds v)) :
∀ᶠ (a : γ) in l, f a < u
theorem eventually_le_of_tendsto_lt {α : Type u} {γ : Type w} [] [] {l : } {f : γα} {u : α} {v : α} (hv : v < u) (h : Filter.Tendsto f l (nhds v)) :
∀ᶠ (a : γ) in l, f a u
theorem Dense.exists_lt {α : Type u} [] [] [] {s : Set α} (hs : ) (x : α) :
ys, y < x
theorem Dense.exists_le {α : Type u} [] [] [] {s : Set α} (hs : ) (x : α) :
ys, y x
theorem Dense.exists_le' {α : Type u} [] [] {s : Set α} (hs : ) (hbot : ∀ (x : α), x s) (x : α) :
ys, 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 #

theorem Ioo_mem_nhdsWithin_Ioi {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ico a c) :
theorem Ioo_mem_nhdsWithin_Ioi' {α : Type u} [] [] {a : α} {b : α} (H : a < b) :
theorem CovBy.nhdsWithin_Ioi {α : Type u} [] [] {a : α} {b : α} (h : a b) :
theorem Ioc_mem_nhdsWithin_Ioi {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ico a c) :
theorem Ioc_mem_nhdsWithin_Ioi' {α : Type u} [] [] {a : α} {b : α} (H : a < b) :
theorem Ico_mem_nhdsWithin_Ioi {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ico a c) :
theorem Ico_mem_nhdsWithin_Ioi' {α : Type u} [] [] {a : α} {b : α} (H : a < b) :
theorem Icc_mem_nhdsWithin_Ioi {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ico a c) :
theorem Icc_mem_nhdsWithin_Ioi' {α : Type u} [] [] {a : α} {b : α} (H : a < b) :
@[simp]
theorem nhdsWithin_Ioc_eq_nhdsWithin_Ioi {α : Type u} [] [] {a : α} {b : α} (h : a < b) :
@[simp]
theorem nhdsWithin_Ioo_eq_nhdsWithin_Ioi {α : Type u} [] [] {a : α} {b : α} (h : a < b) :
@[simp]
theorem continuousWithinAt_Ioc_iff_Ioi {α : Type u} {β : Type v} [] [] [] {a : α} {b : α} {f : αβ} (h : a < b) :
@[simp]
theorem continuousWithinAt_Ioo_iff_Ioi {α : Type u} {β : Type v} [] [] [] {a : α} {b : α} {f : αβ} (h : a < b) :

Point included #

theorem Ico_mem_nhdsWithin_Ici' {α : Type u} [] [] {a : α} {b : α} (H : a < b) :
theorem Ico_mem_nhdsWithin_Ici {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ico a c) :
theorem Ioo_mem_nhdsWithin_Ici {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ioo a c) :
theorem Ioc_mem_nhdsWithin_Ici {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ioo a c) :
theorem Icc_mem_nhdsWithin_Ici {α : Type u} [] [] {a : α} {b : α} {c : α} (H : b Set.Ico a c) :
theorem Icc_mem_nhdsWithin_Ici' {α : Type u} [] [] {a : α} {b : α} (H : a < b) :
@[simp]
theorem nhdsWithin_Icc_eq_nhdsWithin_Ici {α : Type u} [] [] {a : α} {b : α} (h : a < b) :
@[simp]
theorem nhdsWithin_Ico_eq_nhdsWithin_Ici {α : Type u} [] [] {a : α} {b : α} (h : a < b) :
@[simp]
theorem continuousWithinAt_Icc_iff_Ici {α : Type u} {β : Type v} [] [] [] {a : α} {b : α} {f : αβ} (h : a < b) :
@[simp]
theorem continuousWithinAt_Ico_iff_Ici {α : Type u} {β : Type v} [] [] [] {a : α} {b : α} {f : αβ} (h : a < b) :
instance Subtype.instOrderClosedTopology {α : Type u} [] [] [t : ] {p : αProp} :
Equations
• =
theorem isClosed_le_prod {α : Type u} [] [] [t : ] :
IsClosed {p : α × α | p.1 p.2}
theorem isClosed_le {α : Type u} {β : Type v} [] [] [t : ] [] {f : βα} {g : βα} (hf : ) (hg : ) :
IsClosed {b : β | f b g b}
instance instClosedIicTopology {α : Type u} [] [] [t : ] :
Equations
• =
instance instClosedIciTopology {α : Type u} [] [] [t : ] :
Equations
• =
instance instOrderClosedTopologyOrderDual {α : Type u} [] [] [t : ] :
Equations
• =
theorem isClosed_Icc {α : Type u} [] [] [t : ] {a : α} {b : α} :
@[simp]
theorem closure_Icc {α : Type u} [] [] [t : ] (a : α) (b : α) :
theorem le_of_tendsto_of_tendsto {α : Type u} {β : Type v} [] [] [t : ] {f : βα} {g : βα} {b : } {a₁ : α} {a₂ : α} [b.NeBot] (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : f ≤ᶠ[b] g) :
a₁ a₂
theorem tendsto_le_of_eventuallyLE {α : Type u} {β : Type v} [] [] [t : ] {f : βα} {g : βα} {b : } {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.

theorem le_of_tendsto_of_tendsto' {α : Type u} {β : Type v} [] [] [t : ] {f : βα} {g : βα} {b : } {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₂
@[simp]
theorem closure_le_eq {α : Type u} {β : Type v} [] [] [t : ] [] {f : βα} {g : βα} (hf : ) (hg : ) :
closure {b : β | f b g b} = {b : β | f b g b}
theorem closure_lt_subset_le {α : Type u} {β : Type v} [] [] [t : ] [] {f : βα} {g : βα} (hf : ) (hg : ) :
closure {b : β | f b < g b} {b : β | f b g b}
theorem ContinuousWithinAt.closure_le {α : Type u} {β : Type v} [] [] [t : ] [] {f : βα} {g : βα} {s : Set β} {x : β} (hx : x ) (hf : ) (hg : ) (h : ys, f y g y) :
f x g x
theorem IsClosed.isClosed_le {α : Type u} {β : Type v} [] [] [t : ] [] {f : βα} {g : βα} {s : Set β} (hs : ) (hf : ) (hg : ) :
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.

theorem le_on_closure {α : Type u} {β : Type v} [] [] [t : ] [] {f : βα} {g : βα} {s : Set β} (h : xs, f x g x) (hf : ContinuousOn f ()) (hg : ContinuousOn g ()) ⦃x : β (hx : x ) :
f x g x
theorem IsClosed.epigraph {α : Type u} {β : Type v} [] [] [t : ] [] {f : βα} {s : Set β} (hs : ) (hf : ) :
IsClosed {p : β × α | p.1 s f p.1 p.2}
theorem IsClosed.hypograph {α : Type u} {β : Type v} [] [] [t : ] [] {f : βα} {s : Set β} (hs : ) (hf : ) :
IsClosed {p : β × α | p.1 s p.2 f p.1}
@[instance 90]
instance OrderClosedTopology.to_t2Space {α : Type u} [] [] [t : ] :
Equations
• =
theorem isOpen_lt {α : Type u} {β : Type v} [] [] [] {f : βα} {g : βα} (hf : ) (hg : ) :
IsOpen {b : β | f b < g b}
theorem isOpen_lt_prod {α : Type u} [] [] :
IsOpen {p : α × α | p.1 < p.2}
theorem isOpen_Ioo {α : Type u} [] [] {a : α} {b : α} :
@[simp]
theorem interior_Ioo {α : Type u} [] [] {a : α} {b : α} :
theorem Ioo_subset_closure_interior {α : Type u} [] [] {a : α} {b : α} :
theorem Ioo_mem_nhds {α : Type u} [] [] {a : α} {b : α} {x : α} (ha : a < x) (hb : x < b) :
theorem Ioc_mem_nhds {α : Type u} [] [] {a : α} {b : α} {x : α} (ha : a < x) (hb : x < b) :
theorem Ico_mem_nhds {α : Type u} [] [] {a : α} {b : α} {x : α} (ha : a < x) (hb : x < b) :
theorem Icc_mem_nhds {α : Type u} [] [] {a : α} {b : α} {x : α} (ha : a < x) (hb : x < b) :
theorem lt_subset_interior_le {α : Type u} {β : Type v} [] [] {f : βα} {g : βα} [] (hf : ) (hg : ) :
{b : β | f b < g b} interior {b : β | f b g b}
theorem frontier_le_subset_eq {α : Type u} {β : Type v} [] [] {f : βα} {g : βα} [] (hf : ) (hg : ) :
frontier {b : β | f b g b} {b : β | f b = g b}
theorem frontier_Iic_subset {α : Type u} [] [] (a : α) :
frontier () {a}
theorem frontier_Ici_subset {α : Type u} [] [] (a : α) :
frontier () {a}
theorem frontier_lt_subset_eq {α : Type u} {β : Type v} [] [] {f : βα} {g : βα} [] (hf : ) (hg : ) :
frontier {b : β | f b < g b} {b : β | f b = g b}
theorem continuous_if_le {α : Type u} {β : Type v} {γ : Type w} [] [] {f : βα} {g : βα} [] [] [(x : β) → Decidable (f x g x)] {f' : βγ} {g' : βγ} (hf : ) (hg : ) (hf' : ContinuousOn f' {x : β | f x g x}) (hg' : ContinuousOn g' {x : β | g x f x}) (hfg : ∀ (x : β), f x = g xf' x = g' x) :
Continuous fun (x : β) => if f x g x then f' x else g' x
theorem Continuous.if_le {α : Type u} {β : Type v} {γ : Type w} [] [] {f : βα} {g : βα} [] [] [(x : β) → Decidable (f x g x)] {f' : βγ} {g' : βγ} (hf' : ) (hg' : ) (hf : ) (hg : ) (hfg : ∀ (x : β), f x = g xf' x = g' x) :
Continuous fun (x : β) => if f x g x then f' x else g' x
theorem Filter.Tendsto.eventually_lt {α : Type u} {γ : Type w} [] [] {l : } {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
theorem ContinuousAt.eventually_lt {α : Type u} {β : Type v} [] [] {f : βα} {g : βα} [] {x₀ : β} (hf : ContinuousAt f x₀) (hg : ContinuousAt g x₀) (hfg : f x₀ < g x₀) :
∀ᶠ (x : β) in nhds x₀, f x < g x
theorem Continuous.min {α : Type u} {β : Type v} [] [] {f : βα} {g : βα} [] (hf : ) (hg : ) :
Continuous fun (b : β) => min (f b) (g b)
theorem Continuous.max {α : Type u} {β : Type v} [] [] {f : βα} {g : βα} [] (hf : ) (hg : ) :
Continuous fun (b : β) => max (f b) (g b)
theorem continuous_min {α : Type u} [] [] :
Continuous fun (p : α × α) => min p.1 p.2
theorem continuous_max {α : Type u} [] [] :
Continuous fun (p : α × α) => max p.1 p.2
theorem Filter.Tendsto.max {α : Type u} {β : Type v} [] [] {f : βα} {g : βα} {b : } {a₁ : α} {a₂ : α} (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) :
Filter.Tendsto (fun (b : β) => max (f b) (g b)) b (nhds (max a₁ a₂))
theorem Filter.Tendsto.min {α : Type u} {β : Type v} [] [] {f : βα} {g : βα} {b : } {a₁ : α} {a₂ : α} (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) :
Filter.Tendsto (fun (b : β) => min (f b) (g b)) b (nhds (min a₁ a₂))
theorem Filter.Tendsto.max_right {α : Type u} {β : Type v} [] [] {f : βα} {l : } {a : α} (h : Filter.Tendsto f l (nhds a)) :
Filter.Tendsto (fun (i : β) => max a (f i)) l (nhds a)
theorem Filter.Tendsto.max_left {α : Type u} {β : Type v} [] [] {f : βα} {l : } {a : α} (h : Filter.Tendsto f l (nhds a)) :
Filter.Tendsto (fun (i : β) => max (f i) a) l (nhds a)
theorem Filter.tendsto_nhds_max_right {α : Type u} {β : Type v} [] [] {f : βα} {l : } {a : α} (h : Filter.Tendsto f l (nhdsWithin a ())) :
Filter.Tendsto (fun (i : β) => max a (f i)) l (nhdsWithin a ())
theorem Filter.tendsto_nhds_max_left {α : Type u} {β : Type v} [] [] {f : βα} {l : } {a : α} (h : Filter.Tendsto f l (nhdsWithin a ())) :
Filter.Tendsto (fun (i : β) => max (f i) a) l (nhdsWithin a ())
theorem Filter.Tendsto.min_right {α : Type u} {β : Type v} [] [] {f : βα} {l : } {a : α} (h : Filter.Tendsto f l (nhds a)) :
Filter.Tendsto (fun (i : β) => min a (f i)) l (nhds a)
theorem Filter.Tendsto.min_left {α : Type u} {β : Type v} [] [] {f : βα} {l : } {a : α} (h : Filter.Tendsto f l (nhds a)) :
Filter.Tendsto (fun (i : β) => min (f i) a) l (nhds a)
theorem Filter.tendsto_nhds_min_right {α : Type u} {β : Type v} [] [] {f : βα} {l : } {a : α} (h : Filter.Tendsto f l (nhdsWithin a ())) :
Filter.Tendsto (fun (i : β) => min a (f i)) l (nhdsWithin a ())
theorem Filter.tendsto_nhds_min_left {α : Type u} {β : Type v} [] [] {f : βα} {l : } {a : α} (h : Filter.Tendsto f l (nhdsWithin a ())) :
Filter.Tendsto (fun (i : β) => min (f i) a) l (nhdsWithin a ())
theorem Dense.exists_between {α : Type u} [] [] [] {s : Set α} (hs : ) {x : α} {y : α} (h : x < y) :
zs, z Set.Ioo x y
theorem Dense.Ioi_eq_biUnion {α : Type u} [] [] [] {s : Set α} (hs : ) (x : α) :
= ys ,
theorem Dense.Iio_eq_biUnion {α : Type u} [] [] [] {s : Set α} (hs : ) (x : α) :
= ys ,
instance instOrderClosedTopologyProd {α : Type u} {β : Type v} [] [] [] [] :
Equations
• =
instance instOrderClosedTopologyForall {ι : Type u_1} {α : ιType u_2} [(i : ι) → Preorder (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OrderClosedTopology (α i)] :
OrderClosedTopology ((i : ι) → α i)
Equations
• =
instance Pi.orderClosedTopology' {α : Type u} {β : Type v} [] [] :
Equations
• =