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) [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.

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.

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.

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

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

theorem Dense.orderDual {α : Type u} [TopologicalSpace α] {s : Set α} (hs : Dense s) : Dense (⇑OrderDual.ofDual ⁻¹' s)

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

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

theorem isClosed_Iic {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {a : α} : IsClosed (Set.Iic a)

@[deprecated ClosedIicTopology.isClosed_Iic]

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

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

@[simp]

theorem closure_Iic {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] (a : α) : closure (Set.Iic a) = Set.Iic a

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

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

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

@[simp]

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

@[simp]

theorem bddAbove_closure {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s : Set α} : BddAbove (closure s) ↔ BddAbove s

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

Alias of the reverse direction of bddAbove_closure.

@[simp]

theorem disjoint_nhds_atBot_iff {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {a : α} : Disjoint (nhds a) Filter.atBot ↔ ¬IsBot a

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

theorem disjoint_nhds_atBot {α : Type u} [Preorder α] [NoBotOrder α] [TopologicalSpace α] [ClosedIicTopology α] (a : α) : Disjoint (nhds a) Filter.atBot

@[simp]

theorem inf_nhds_atBot {α : Type u} [Preorder α] [NoBotOrder α] [TopologicalSpace α] [ClosedIicTopology α] (a : α) : nhds a ⊓ Filter.atBot = ⊥

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)

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

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

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

theorem isOpen_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} : IsOpen (Set.Ioi a)

@[simp]

theorem interior_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} : interior (Set.Ioi a) = Set.Ioi a

theorem Ioi_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (h : a < b) : Set.Ioi a ∈ nhds b

theorem eventually_gt_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (hab : b < a) : ∀ᶠ (x : α) in nhds a, b < x

theorem Ici_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (h : a < b) : Set.Ici a ∈ nhds b

theorem eventually_ge_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (hab : b < a) : ∀ᶠ (x : α) in nhds a, b ≤ x

theorem Filter.Tendsto.eventually_const_lt {α : 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

@[deprecated Filter.Tendsto.eventually_const_lt]

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

Alias of Filter.Tendsto.eventually_const_lt.

theorem Filter.Tendsto.eventually_const_le {α : 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

@[deprecated Filter.Tendsto.eventually_const_le]

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

Alias of Filter.Tendsto.eventually_const_le.

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

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

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

theorem Ioo_mem_nhdsWithin_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) : Set.Ioo a b ∈ nhdsWithin b (Set.Iio b)

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)

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

theorem PredOrder.nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} [PredOrder α] : nhdsWithin a (Set.Iio a) = ⊥

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)

theorem Ico_mem_nhdsWithin_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) : Set.Ico a b ∈ nhdsWithin b (Set.Iio b)

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)

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

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)

theorem Icc_mem_nhdsWithin_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) : Set.Icc a b ∈ nhdsWithin b (Set.Iio b)

@[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)

@[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)

@[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

@[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

theorem CovBy.nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a ⋖ b) : nhdsWithin b (Set.Iic b) = pure b

theorem PredOrder.nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {b : α} [PredOrder α] : nhdsWithin b (Set.Iic b) = pure b

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

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)

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)

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)

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)

theorem Icc_mem_nhdsWithin_Iic' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) : Set.Icc a b ∈ nhdsWithin b (Set.Iic b)

@[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)

@[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)

@[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

@[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

theorem isClosed_Ici {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {a : α} : IsClosed (Set.Ici a)

@[deprecated]

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

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

@[simp]

theorem closure_Ici {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] (a : α) : closure (Set.Ici a) = Set.Ici a

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

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

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

@[simp]

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

@[simp]

theorem bddBelow_closure {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {s : Set α} : BddBelow (closure s) ↔ BddBelow s

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

Alias of the reverse direction of bddBelow_closure.

@[simp]

theorem disjoint_nhds_atTop_iff {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {a : α} : Disjoint (nhds a) Filter.atTop ↔ ¬IsTop a

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

theorem disjoint_nhds_atTop {α : Type u} [Preorder α] [NoTopOrder α] [TopologicalSpace α] [ClosedIciTopology α] (a : α) : Disjoint (nhds a) Filter.atTop

@[simp]

theorem inf_nhds_atTop {α : Type u} [Preorder α] [NoTopOrder α] [TopologicalSpace α] [ClosedIciTopology α] (a : α) : nhds a ⊓ Filter.atTop = ⊥

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)

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

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

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

theorem isOpen_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} : IsOpen (Set.Iio a)

@[simp]

theorem interior_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} : interior (Set.Iio a) = Set.Iio a

theorem Iio_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (h : a < b) : Set.Iio b ∈ nhds a

theorem eventually_lt_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (hab : a < b) : ∀ᶠ (x : α) in nhds a, x < b

theorem Iic_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (h : a < b) : Set.Iic b ∈ nhds a

theorem eventually_le_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (hab : a < b) : ∀ᶠ (x : α) in nhds a, x ≤ b

theorem Filter.Tendsto.eventually_lt_const {α : 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

@[deprecated Filter.Tendsto.eventually_lt_const]

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

Alias of Filter.Tendsto.eventually_lt_const.

theorem Filter.Tendsto.eventually_le_const {α : 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

@[deprecated Filter.Tendsto.eventually_le_const]

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

Alias of Filter.Tendsto.eventually_le_const.

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

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

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

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)

theorem Ioo_mem_nhdsWithin_Ioi' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (H : a < b) : Set.Ioo a b ∈ nhdsWithin a (Set.Ioi a)

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

theorem SuccOrder.nhdsWithin_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} [SuccOrder α] : nhdsWithin a (Set.Ioi a) = ⊥

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)

theorem Ioc_mem_nhdsWithin_Ioi' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (H : a < b) : Set.Ioc a b ∈ nhdsWithin a (Set.Ioi a)

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)

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

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)

theorem Icc_mem_nhdsWithin_Ioi' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (H : a < b) : Set.Icc a b ∈ nhdsWithin a (Set.Ioi a)

@[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)

@[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)

@[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

@[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

theorem CovBy.nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (H : a ⋖ b) : nhdsWithin a (Set.Ici a) = pure a

theorem SuccOrder.nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} [SuccOrder α] : nhdsWithin a (Set.Ici a) = pure a

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

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)

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)

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)

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)

theorem Icc_mem_nhdsWithin_Ici' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (H : a < b) : Set.Icc a b ∈ nhdsWithin a (Set.Ici a)

@[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)

@[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)

@[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

@[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

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

theorem isClosed_le_prod {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] : IsClosed {p : α × α | p.1 ≤ p.2}

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}

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

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

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

theorem isClosed_Icc {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {a b : α} : IsClosed (Set.Icc a b)

@[simp]

theorem closure_Icc {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] (a b : α) : closure (Set.Icc a b) = Set.Icc a b

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₂

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.

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₂

@[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}

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}

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

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.

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

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}

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}

@[instance 90]

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

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}

theorem isOpen_lt_prod {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] : IsOpen {p : α × α | p.1 < p.2}

theorem isOpen_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a b : α} : IsOpen (Set.Ioo a b)

@[simp]

theorem interior_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a b : α} : interior (Set.Ioo a b) = Set.Ioo a b

theorem Ioo_subset_closure_interior {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a b : α} : Set.Ioo a b ⊆ closure (interior (Set.Ioo a b))

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

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

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

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

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.

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}

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}

theorem frontier_Iic_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] (a : α) : frontier (Set.Iic a) ⊆ {a}

theorem frontier_Ici_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] (a : α) : frontier (Set.Ici a) ⊆ {a}

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}

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

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

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

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

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

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

theorem continuous_min {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] : Continuous fun (p : α × α) => p.1 ⊓ p.2

theorem continuous_max {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] : Continuous fun (p : α × α) => p.1 ⊔ p.2

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₂))

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₂))

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)

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)

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))

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))

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)

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)

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))

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))

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

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

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

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

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

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