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.

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)

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 (since := "2024-11-17")]

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 (since := "2024-11-17")]

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_nhdsLT {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) : Set.Ioo a b ∈ nhdsWithin b (Set.Iio b)

@[deprecated Ioo_mem_nhdsLT (since := "2024-12-21")]

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

Alias of Ioo_mem_nhdsLT.

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)

@[deprecated Ioo_mem_nhdsLT_of_mem (since := "2024-12-21")]

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)

Alias of Ioo_mem_nhdsLT_of_mem.

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

@[deprecated CovBy.nhdsLT (since := "2024-12-21")]

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

Alias of CovBy.nhdsLT.

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

@[deprecated PredOrder.nhdsLT (since := "2024-12-21")]

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

Alias of PredOrder.nhdsLT.

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)

@[deprecated Ico_mem_nhdsLT_of_mem (since := "2024-12-21")]

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)

Alias of Ico_mem_nhdsLT_of_mem.

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

@[deprecated Ico_mem_nhdsLT (since := "2024-12-21")]

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

Alias of Ico_mem_nhdsLT.

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)

@[deprecated Ioc_mem_nhdsLT_of_mem (since := "2024-12-21")]

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)

Alias of Ioc_mem_nhdsLT_of_mem.

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

@[deprecated Ioc_mem_nhdsLT (since := "2024-12-21")]

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

Alias of Ioc_mem_nhdsLT.

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)

@[deprecated Icc_mem_nhdsLT_of_mem (since := "2024-12-21")]

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)

Alias of Icc_mem_nhdsLT_of_mem.

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

@[deprecated Icc_mem_nhdsLT (since := "2024-12-21")]

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

Alias of Icc_mem_nhdsLT.

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

@[deprecated nhdsWithin_Ico_eq_nhdsLT (since := "2024-12-21")]

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)

Alias of nhdsWithin_Ico_eq_nhdsLT.

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

@[deprecated nhdsWithin_Ioo_eq_nhdsLT (since := "2024-12-21")]

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)

Alias of nhdsWithin_Ioo_eq_nhdsLT.

@[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.nhdsLE {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a ⋖ b) : nhdsWithin b (Set.Iic b) = pure b

@[deprecated CovBy.nhdsLE (since := "2024-12-21")]

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

Alias of CovBy.nhdsLE.

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

@[deprecated PredOrder.nhdsLE (since := "2024-12-21")]

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

Alias of PredOrder.nhdsLE.

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

@[deprecated Ioc_mem_nhdsLE (since := "2024-12-21")]

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

Alias of Ioc_mem_nhdsLE.

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)

@[deprecated Ioo_mem_nhdsLE_of_mem (since := "2024-12-21")]

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)

Alias of Ioo_mem_nhdsLE_of_mem.

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)

@[deprecated Ico_mem_nhdsLE_of_mem (since := "2024-12-22")]

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)

Alias of Ico_mem_nhdsLE_of_mem.

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)

@[deprecated Ioc_mem_nhdsLE_of_mem (since := "2024-12-22")]

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)

Alias of Ioc_mem_nhdsLE_of_mem.

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)

@[deprecated Icc_mem_nhdsLE_of_mem (since := "2024-12-22")]

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)

Alias of Icc_mem_nhdsLE_of_mem.

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

@[deprecated Icc_mem_nhdsLE (since := "2024-12-22")]

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

Alias of Icc_mem_nhdsLE.

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

@[deprecated nhdsWithin_Icc_eq_nhdsLE (since := "2024-12-22")]

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)

Alias of nhdsWithin_Icc_eq_nhdsLE.

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

@[deprecated nhdsWithin_Ioc_eq_nhdsLE (since := "2024-12-22")]

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)

Alias of nhdsWithin_Ioc_eq_nhdsLE.

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

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 (since := "2024-11-17")]

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 (since := "2024-11-17")]

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

@[deprecated Ioo_mem_nhdsGT_of_mem (since := "2024-12-22")]

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)

Alias of Ioo_mem_nhdsGT_of_mem.

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

@[deprecated Ioo_mem_nhdsGT (since := "2024-12-22")]

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

Alias of Ioo_mem_nhdsGT.

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

@[deprecated CovBy.nhdsGT (since := "2024-12-22")]

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

Alias of CovBy.nhdsGT.

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

@[deprecated SuccOrder.nhdsGT (since := "2024-12-22")]

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

Alias of SuccOrder.nhdsGT.

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)

@[deprecated Ioc_mem_nhdsGT_of_mem (since := "2024-12-22")]

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)

Alias of Ioc_mem_nhdsGT_of_mem.

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

@[deprecated Ioc_mem_nhdsGT (since := "2024-12-22")]

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

Alias of Ioc_mem_nhdsGT.

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)

@[deprecated Ico_mem_nhdsGT_of_mem (since := "2024-12-22")]

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)

Alias of Ico_mem_nhdsGT_of_mem.

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

@[deprecated Ico_mem_nhdsGT (since := "2024-12-22")]

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

Alias of Ico_mem_nhdsGT.

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)

@[deprecated Icc_mem_nhdsGT_of_mem (since := "2024-12-22")]

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)

Alias of Icc_mem_nhdsGT_of_mem.

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

@[deprecated Icc_mem_nhdsGT (since := "2024-12-22")]

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

Alias of Icc_mem_nhdsGT.

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

@[deprecated nhdsWithin_Ioc_eq_nhdsGT (since := "2024-12-22")]

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)

Alias of nhdsWithin_Ioc_eq_nhdsGT.

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

@[deprecated nhdsWithin_Ioo_eq_nhdsGT (since := "2024-12-22")]

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)

Alias of nhdsWithin_Ioo_eq_nhdsGT.

@[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.nhdsGE {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (H : a ⋖ b) : nhdsWithin a (Set.Ici a) = pure a

@[deprecated CovBy.nhdsGE (since := "2024-12-22")]

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

Alias of CovBy.nhdsGE.

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

@[deprecated SuccOrder.nhdsGE (since := "2024-12-22")]

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

Alias of SuccOrder.nhdsGE.

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

@[deprecated Ico_mem_nhdsGE (since := "2024-12-22")]

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

Alias of Ico_mem_nhdsGE.

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)

@[deprecated Ico_mem_nhdsGE_of_mem (since := "2024-12-22")]

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)

Alias of Ico_mem_nhdsGE_of_mem.

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)

@[deprecated Ioo_mem_nhdsGE_of_mem (since := "2024-12-22")]

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)

Alias of Ioo_mem_nhdsGE_of_mem.

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)

@[deprecated Ioc_mem_nhdsGE_of_mem (since := "2024-12-22")]

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)

Alias of Ioc_mem_nhdsGE_of_mem.

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)

@[deprecated Icc_mem_nhdsGE_of_mem (since := "2024-12-22")]

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)

Alias of Icc_mem_nhdsGE_of_mem.

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

@[deprecated Icc_mem_nhdsGE (since := "2024-12-22")]

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

Alias of Icc_mem_nhdsGE.

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

@[deprecated nhdsWithin_Icc_eq_nhdsGE (since := "2024-12-22")]

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)

Alias of nhdsWithin_Icc_eq_nhdsGE.

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

@[deprecated nhdsWithin_Ico_eq_nhdsGE (since := "2024-12-22")]

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)

Alias of nhdsWithin_Ico_eq_nhdsGE.

@[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 (α → β)