Documentation

Mathlib.Topology.Order.Basic

Theory of topology on ordered spaces #

Main definitions #

The order topology on an ordered space is the topology generated by all open intervals (or equivalently by those of the form (-∞, a) and (b, +∞)). We define it as Preorder.topology α. However, we do not register it as an instance (as many existing ordered types already have topologies, which would be equal but not definitionally equal to Preorder.topology α). Instead, we introduce a class OrderTopology α (which is a Prop, also known as a mixin) saying that on the type α having already a topological space structure and a preorder structure, the topological structure is equal to the order topology.

We also introduce another (mixin) class OrderClosedTopology α saying that the set of points (x, y) with x ≤ y is closed in the product space. This is automatically satisfied on a linear order with the order topology.

We prove many basic properties of such topologies.

Main statements #

This file contains the proofs of the following facts. For exact requirements (OrderClosedTopology vs OrderTopology, Preorder vs PartialOrder vs LinearOrder etc) see their statements.

Open / closed sets #

Convergence and inequalities #

Min, max, sSup and sInf #

Implementation notes #

We do not register the order topology as an instance on a preorder (or even on a linear order). Indeed, on many such spaces, a topology has already been constructed in a different way (think of the discrete spaces or , or that could inherit a topology as the completion of ), and is in general not defeq to the one generated by the intervals. We make it available as a definition Preorder.topology α though, that can be registered as an instance when necessary, or for specific types.

  • isClosed_le' : ∀ (a : α), IsClosed {b | b a}

    For any a, the set {b | b ≤ a} is closed.

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

Instances
    • isClosed_ge' : ∀ (a : α), IsClosed {b | a b}

      For any a, the set {b | a ≤ b} is closed.

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

    Instances
      • isClosed_le' : IsClosed {p | p.fst p.snd}

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

      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.

      Instances
        theorem Dense.orderDual {α : Type u} [TopologicalSpace α] {s : Set α} (hs : Dense s) :
        Dense (OrderDual.ofDual ⁻¹' s)
        theorem isClosed_Iic {α : Type u} [TopologicalSpace α] [Preorder α] [t : ClosedIicTopology α] {a : α} :
        @[simp]
        theorem closure_Iic {α : Type u} [TopologicalSpace α] [Preorder α] [t : ClosedIicTopology α] (a : α) :
        theorem le_of_tendsto {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : ClosedIicTopology α] {f : βα} {a : α} {b : α} {x : Filter β} [Filter.NeBot 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} [TopologicalSpace α] [Preorder α] [t : ClosedIicTopology α] {f : βα} {a : α} {b : α} {x : Filter β} [Filter.NeBot x] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ (c : β), f c b) :
        a b
        theorem isClosed_Ici {α : Type u} [TopologicalSpace α] [Preorder α] [t : ClosedIciTopology α] {a : α} :
        @[simp]
        theorem closure_Ici {α : Type u} [TopologicalSpace α] [Preorder α] [t : ClosedIciTopology α] (a : α) :
        theorem ge_of_tendsto {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : ClosedIciTopology α] {f : βα} {a : α} {b : α} {x : Filter β} [Filter.NeBot 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} [TopologicalSpace α] [Preorder α] [t : ClosedIciTopology α] {f : βα} {a : α} {b : α} {x : Filter β} [Filter.NeBot x] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ (c : β), b f c) :
        b a
        theorem isClosed_le_prod {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] :
        IsClosed {p | p.fst p.snd}
        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}
        theorem isClosed_Icc {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {a : α} {b : α} :
        @[simp]
        theorem closure_Icc {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] (a : α) (b : α) :
        theorem le_of_tendsto_of_tendsto {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f : βα} {g : βα} {b : Filter β} {a₁ : α} {a₂ : α} [Filter.NeBot b] (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₂ : α} [Filter.NeBot b] (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₂ : α} [Filter.NeBot b] (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 : β), y sf 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 : β), x sf 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.fst s f p.fst p.snd}
        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.fst s p.snd f p.fst}
        theorem nhdsWithin_Ici_neBot {α : Type u} [TopologicalSpace α] [Preorder α] {a : α} {b : α} (H₂ : a b) :
        theorem nhdsWithin_Iic_neBot {α : Type u} [TopologicalSpace α] [Preorder α] {a : α} {b : α} (H : a b) :
        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.fst < p.snd}
        theorem isOpen_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} :
        @[simp]
        @[simp]
        @[simp]
        theorem interior_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} :
        theorem Iio_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
        theorem Ioi_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
        theorem Iic_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
        theorem Ici_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
        theorem Ioo_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {x : α} (ha : a < x) (hb : x < b) :
        theorem Ioc_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {x : α} (ha : a < x) (hb : x < b) :
        theorem Ico_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {x : α} (ha : a < x) (hb : x < b) :
        theorem Icc_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {x : α} (ha : a < x) (hb : x < b) :
        theorem eventually_lt_of_tendsto_lt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {l : Filter γ} {f : γα} {u : α} {v : α} (hv : v < u) (h : Filter.Tendsto f l (nhds v)) :
        ∀ᶠ (a : γ) in l, f a < u
        theorem eventually_gt_of_tendsto_gt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {l : Filter γ} {f : γα} {u : α} {v : α} (hv : u < v) (h : Filter.Tendsto f l (nhds v)) :
        ∀ᶠ (a : γ) in l, u < f a
        theorem eventually_le_of_tendsto_lt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {l : Filter γ} {f : γα} {u : α} {v : α} (hv : v < u) (h : Filter.Tendsto f l (nhds v)) :
        ∀ᶠ (a : γ) in l, f a u
        theorem eventually_ge_of_tendsto_gt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {l : Filter γ} {f : γα} {u : α} {v : α} (hv : u < v) (h : Filter.Tendsto f l (nhds v)) :
        ∀ᶠ (a : γ) in l, u f a

        Neighborhoods to the left and to the right on an OrderClosedTopology #

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

        Right neighborhoods, point excluded #

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

        Left neighborhoods, point excluded #

        theorem Ioo_mem_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (H : b Set.Ioc a c) :
        theorem Ioo_mem_nhdsWithin_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (H : a < b) :
        theorem Covby.nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (h : a b) :
        theorem Ico_mem_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (H : b Set.Ioc a c) :
        theorem Ico_mem_nhdsWithin_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (H : a < b) :
        theorem Ioc_mem_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (H : b Set.Ioc a c) :
        theorem Ioc_mem_nhdsWithin_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (H : a < b) :
        theorem Icc_mem_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (H : b Set.Ioc a c) :
        theorem Icc_mem_nhdsWithin_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (H : a < b) :
        @[simp]
        theorem nhdsWithin_Ico_eq_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
        @[simp]
        theorem nhdsWithin_Ioo_eq_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
        @[simp]
        theorem continuousWithinAt_Ico_iff_Iio {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [TopologicalSpace γ] {a : α} {b : α} {f : αγ} (h : a < b) :
        @[simp]
        theorem continuousWithinAt_Ioo_iff_Iio {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [TopologicalSpace γ] {a : α} {b : α} {f : αγ} (h : a < b) :

        Right neighborhoods, point included #

        theorem Ioo_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (H : b Set.Ioo a c) :
        theorem Ioc_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (H : b Set.Ioo a c) :
        theorem Ico_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (H : b Set.Ico a c) :
        theorem Ico_mem_nhdsWithin_Ici' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (H : a < b) :
        theorem Icc_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (H : b Set.Ico a c) :
        theorem Icc_mem_nhdsWithin_Ici' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (H : a < b) :
        @[simp]
        theorem nhdsWithin_Icc_eq_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
        @[simp]
        theorem nhdsWithin_Ico_eq_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
        @[simp]
        theorem continuousWithinAt_Icc_iff_Ici {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [TopologicalSpace β] {a : α} {b : α} {f : αβ} (h : a < b) :
        @[simp]
        theorem continuousWithinAt_Ico_iff_Ici {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [TopologicalSpace β] {a : α} {b : α} {f : αβ} (h : a < b) :

        Left neighborhoods, point included #

        theorem Ioo_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (H : b Set.Ioo a c) :
        theorem Ico_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (H : b Set.Ioo a c) :
        theorem Ioc_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (H : b Set.Ioc a c) :
        theorem Ioc_mem_nhdsWithin_Iic' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (H : a < b) :
        theorem Icc_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {c : α} (H : b Set.Ioc a c) :
        theorem Icc_mem_nhdsWithin_Iic' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (H : a < b) :
        @[simp]
        theorem nhdsWithin_Icc_eq_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
        @[simp]
        theorem nhdsWithin_Ioc_eq_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (h : a < b) :
        @[simp]
        theorem continuousWithinAt_Icc_iff_Iic {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [TopologicalSpace β] {a : α} {b : α} {f : αβ} (h : a < b) :
        @[simp]
        theorem continuousWithinAt_Ioc_iff_Iic {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [TopologicalSpace β] {a : α} {b : α} {f : αβ} (h : a < b) :
        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_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 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} [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 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} [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 => min (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 => max (f b) (g b)
        theorem continuous_min {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] :
        Continuous fun p => min p.fst p.snd
        theorem continuous_max {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] :
        Continuous fun p => max p.fst p.snd
        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 => max (f b) (g b)) b (nhds (max 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 => min (f b) (g b)) b (nhds (min 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 => max 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 => max (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 => max 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 => max (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 => min 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 => min (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 => min 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 => min (f i) a) l (nhdsWithin a (Set.Iio a))
        theorem Dense.exists_lt {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) :
        y, y s y < x
        theorem Dense.exists_gt {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) :
        y, y s x < y
        theorem Dense.exists_le {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) :
        y, y s y x
        theorem Dense.exists_ge {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) :
        y, y s x y
        theorem Dense.exists_le' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {s : Set α} (hs : Dense s) (hbot : ∀ (x : α), IsBot xx s) (x : α) :
        y, y s y x
        theorem Dense.exists_ge' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {s : Set α} (hs : Dense s) (htop : ∀ (x : α), IsTop xx s) (x : α) :
        y, y s x y
        theorem Dense.exists_between {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) {x : α} {y : α} (h : x < y) :
        z, 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 : α) (_ : 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 : α) (_ : y s Set.Iio x), Set.Iio y
        instance instOrderClosedTopologyForAllTopologicalSpacePreorder {ι : Type u_1} {α : ιType u_2} [(i : ι) → Preorder (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OrderClosedTopology (α i)] :
        OrderClosedTopology ((i : ι) → α i)
        class OrderTopology (α : Type u_1) [t : TopologicalSpace α] [Preorder α] :

        The order topology on an ordered type is the topology generated by open intervals. We register it on a preorder, but it is mostly interesting in linear orders, where it is also order-closed. We define it as a mixin. If you want to introduce the order topology on a preorder, use Preorder.topology.

        Instances

          (Order) topology on a partial order α generated by the subbase of open intervals (a, ∞) = { x ∣ a < x }, (-∞ , b) = {x ∣ x < b} for all a, b in α. We do not register it as an instance as many ordered sets are already endowed with the same topology, most often in a non-defeq way though. Register as a local instance when necessary.

          Instances For
            theorem isOpen_lt' {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] (a : α) :
            IsOpen {b | a < b}
            theorem isOpen_gt' {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] (a : α) :
            IsOpen {b | b < a}
            theorem lt_mem_nhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {a : α} {b : α} (h : a < b) :
            ∀ᶠ (x : α) in nhds b, a < x
            theorem le_mem_nhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {a : α} {b : α} (h : a < b) :
            ∀ᶠ (x : α) in nhds b, a x
            theorem gt_mem_nhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {a : α} {b : α} (h : a < b) :
            ∀ᶠ (x : α) in nhds a, x < b
            theorem ge_mem_nhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {a : α} {b : α} (h : a < b) :
            ∀ᶠ (x : α) in nhds a, x b
            theorem nhds_eq_order {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] (a : α) :
            nhds a = (⨅ (b : α) (_ : b Set.Iio a), Filter.principal (Set.Ioi b)) ⨅ (b : α) (_ : b Set.Ioi a), Filter.principal (Set.Iio b)
            theorem tendsto_order {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {f : βα} {a : α} {x : Filter β} :
            Filter.Tendsto f x (nhds a) (∀ (a' : α), a' < a∀ᶠ (b : β) in x, a' < f b) ∀ (a' : α), a' > a∀ᶠ (b : β) in x, f b < a'
            instance tendstoIccClassNhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] (a : α) :
            instance tendstoIcoClassNhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] (a : α) :
            instance tendstoIocClassNhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] (a : α) :
            instance tendstoIooClassNhds {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] (a : α) :
            theorem tendsto_of_tendsto_of_tendsto_of_le_of_le' {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {f : βα} {g : βα} {h : βα} {b : Filter β} {a : α} (hg : Filter.Tendsto g b (nhds a)) (hh : Filter.Tendsto h b (nhds a)) (hgf : ∀ᶠ (b : β) in b, g b f b) (hfh : ∀ᶠ (b : β) in b, f b h b) :

            Squeeze theorem (also known as sandwich theorem). This version assumes that inequalities hold eventually for the filter.

            theorem tendsto_of_tendsto_of_tendsto_of_le_of_le {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {f : βα} {g : βα} {h : βα} {b : Filter β} {a : α} (hg : Filter.Tendsto g b (nhds a)) (hh : Filter.Tendsto h b (nhds a)) (hgf : g f) (hfh : f h) :

            Squeeze theorem (also known as sandwich theorem). This version assumes that inequalities hold everywhere.

            theorem nhds_order_unbounded {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {a : α} (hu : u, a < u) (hl : l, l < a) :
            nhds a = ⨅ (l : α) (_ : l < a) (u : α) (_ : a < u), Filter.principal (Set.Ioo l u)
            theorem tendsto_order_unbounded {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {f : βα} {a : α} {x : Filter β} (hu : u, a < u) (hl : l, l < a) (h : ∀ (l u : α), l < aa < u∀ᶠ (b : β) in x, l < f b f b < u) :
            instance tendstoIxxNhdsWithin {α : Type u_1} [Preorder α] [TopologicalSpace α] (a : α) {s : Set α} {t : Set α} {Ixx : ααSet α} [Filter.TendstoIxxClass Ixx (nhds a) (nhds a)] [Filter.TendstoIxxClass Ixx (Filter.principal s) (Filter.principal t)] :
            instance tendstoIccClassNhdsPi {ι : Type u_1} {α : ιType u_2} [(i : ι) → Preorder (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OrderTopology (α i)] (f : (i : ι) → α i) :
            theorem induced_topology_le_preorder {α : Type u} {β : Type v} [Preorder α] [Preorder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : ∀ {x y : α}, f x < f y x < y) :
            theorem induced_topology_eq_preorder {α : Type u} {β : Type v} [Preorder α] [Preorder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : ∀ {x y : α}, f x < f y x < y) (H₁ : ∀ {a : α} {b : β} {x : α}, b < f a¬b < f xy, y < a b f y) (H₂ : ∀ {a : α} {b : β} {x : α}, f a < b¬f x < by, a < y f y b) :
            theorem induced_orderTopology' {α : Type u} {β : Type v} [Preorder α] [ta : TopologicalSpace β] [Preorder β] [OrderTopology β] (f : αβ) (hf : ∀ {x y : α}, f x < f y x < y) (H₁ : ∀ {a : α} {x : β}, x < f ab, b < a x f b) (H₂ : ∀ {a : α} {x : β}, f a < xb, b > a f b x) :
            theorem induced_orderTopology {α : Type u} {β : Type v} [Preorder α] [ta : TopologicalSpace β] [Preorder β] [OrderTopology β] (f : αβ) (hf : ∀ {x y : α}, f x < f y x < y) (H : ∀ {x y : β}, x < ya, x < f a f a < y) :

            The topology induced by a strictly monotone function with order-connected range is the preorder topology.

            theorem StrictMono.embedding_of_ordConnected {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [TopologicalSpace α] [h : OrderTopology α] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : StrictMono f) (hc : Set.OrdConnected (Set.range f)) :

            A strictly monotone function between linear orders with order topology is a topological embedding provided that the range of f is order-connected.

            On a Set.OrdConnected subset of a linear order, the order topology for the restriction of the order is the same as the restriction to the subset of the order topology.

            theorem nhdsWithin_Ici_eq'' {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
            nhdsWithin a (Set.Ici a) = (⨅ (u : α) (_ : a < u), Filter.principal (Set.Iio u)) Filter.principal (Set.Ici a)
            theorem nhdsWithin_Iic_eq'' {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
            nhdsWithin a (Set.Iic a) = (⨅ (l : α) (_ : l < a), Filter.principal (Set.Ioi l)) Filter.principal (Set.Iic a)
            theorem nhdsWithin_Ici_eq' {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (ha : u, a < u) :
            nhdsWithin a (Set.Ici a) = ⨅ (u : α) (_ : a < u), Filter.principal (Set.Ico a u)
            theorem nhdsWithin_Iic_eq' {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (ha : l, l < a) :
            nhdsWithin a (Set.Iic a) = ⨅ (l : α) (_ : l < a), Filter.principal (Set.Ioc l a)
            theorem nhdsWithin_Ici_basis' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : u, a < u) :
            Filter.HasBasis (nhdsWithin a (Set.Ici a)) (fun u => a < u) fun u => Set.Ico a u
            theorem nhdsWithin_Iic_basis' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : l, l < a) :
            Filter.HasBasis (nhdsWithin a (Set.Iic a)) (fun l => l < a) fun l => Set.Ioc l a
            theorem nhdsWithin_Ici_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) :
            Filter.HasBasis (nhdsWithin a (Set.Ici a)) (fun u => a < u) fun u => Set.Ico a u
            theorem nhdsWithin_Iic_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] (a : α) :
            Filter.HasBasis (nhdsWithin a (Set.Iic a)) (fun l => l < a) fun l => Set.Ioc l a
            theorem nhds_top_order {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTop α] [OrderTopology α] :
            nhds = ⨅ (l : α) (_ : l < ), Filter.principal (Set.Ioi l)
            theorem nhds_bot_order {α : Type u} [TopologicalSpace α] [Preorder α] [OrderBot α] [OrderTopology α] :
            nhds = ⨅ (l : α) (_ : < l), Filter.principal (Set.Iio l)
            theorem nhds_top_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] [Nontrivial α] :
            Filter.HasBasis (nhds ) (fun a => a < ) fun a => Set.Ioi a
            theorem nhds_bot_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] [Nontrivial α] :
            Filter.HasBasis (nhds ) (fun a => < a) fun a => Set.Iio a
            theorem tendsto_nhds_top_mono {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] {l : Filter α} {f : αβ} {g : αβ} (hf : Filter.Tendsto f l (nhds )) (hg : f ≤ᶠ[l] g) :
            theorem tendsto_nhds_bot_mono {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β] {l : Filter α} {f : αβ} {g : αβ} (hf : Filter.Tendsto f l (nhds )) (hg : g ≤ᶠ[l] f) :
            theorem tendsto_nhds_top_mono' {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] {l : Filter α} {f : αβ} {g : αβ} (hf : Filter.Tendsto f l (nhds )) (hg : f g) :
            theorem tendsto_nhds_bot_mono' {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β] {l : Filter α} {f : αβ} {g : αβ} (hf : Filter.Tendsto f l (nhds )) (hg : g f) :
            theorem eventually_le_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (hab : a < b) :
            ∀ᶠ (x : α) in nhds a, x b
            theorem eventually_lt_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (hab : a < b) :
            ∀ᶠ (x : α) in nhds a, x < b
            theorem eventually_ge_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (hab : b < a) :
            ∀ᶠ (x : α) in nhds a, b x
            theorem eventually_gt_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} (hab : b < a) :
            ∀ᶠ (x : α) in nhds a, b < x
            theorem order_separated {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a₁ : α} {a₂ : α} (h : a₁ < a₂) :
            u v, IsOpen u IsOpen v a₁ u a₂ v ∀ (b₁ : α), b₁ u∀ (b₂ : α), b₂ vb₁ < b₂
            theorem exists_Ioc_subset_of_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s nhds a) (h : l, l < a) :
            l, l < a Set.Ioc l a s
            theorem exists_Ioc_subset_of_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s nhds a) {l : α} (hl : l < a) :
            l', l' Set.Ico l a Set.Ioc l' a s
            theorem exists_Ico_subset_of_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s nhds a) {u : α} (hu : a < u) :
            u', u' Set.Ioc a u Set.Ico a u' s
            theorem exists_Ico_subset_of_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s nhds a) (h : u, a < u) :
            u, a < u Set.Ico a u s
            theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s nhdsWithin a (Set.Ici a)) :
            b, a b Set.Icc a b nhdsWithin a (Set.Ici a) Set.Icc a b s
            theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s nhdsWithin a (Set.Iic a)) :
            b, b a Set.Icc b a nhdsWithin a (Set.Iic a) Set.Icc b a s
            theorem exists_Icc_mem_subset_of_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s nhds a) :
            b c, a Set.Icc b c Set.Icc b c nhds a Set.Icc b c s
            theorem IsOpen.exists_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Nontrivial α] {s : Set α} (hs : IsOpen s) (h : Set.Nonempty s) :
            a b, a < b Set.Ioo a b s
            theorem dense_of_exists_between {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Nontrivial α] {s : Set α} (h : ∀ ⦃a b : α⦄, a < bc, c s a < c c < b) :
            theorem dense_iff_exists_between {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [Nontrivial α] {s : Set α} :
            Dense s ∀ (a b : α), a < bc, c s a < c c < b

            A set in a nontrivial densely linear ordered type is dense in the sense of topology if and only if for any a < b there exists c ∈ s, a < c < b. Each implication requires less typeclass assumptions.

            theorem mem_nhds_iff_exists_Ioo_subset' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hl : l, l < a) (hu : u, a < u) :
            s nhds a l u, a Set.Ioo l u Set.Ioo l u s

            A set is a neighborhood of a if and only if it contains an interval (l, u) containing a, provided a is neither a bottom element nor a top element.

            theorem mem_nhds_iff_exists_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α} {s : Set α} :
            s nhds a l u, a Set.Ioo l u Set.Ioo l u s

            A set is a neighborhood of a if and only if it contains an interval (l, u) containing a.

            theorem nhds_basis_Ioo' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (hl : l, l < a) (hu : u, a < u) :
            Filter.HasBasis (nhds a) (fun b => b.fst < a a < b.snd) fun b => Set.Ioo b.fst b.snd
            theorem nhds_basis_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] (a : α) :
            Filter.HasBasis (nhds a) (fun b => b.fst < a a < b.snd) fun b => Set.Ioo b.fst b.snd
            theorem Filter.Eventually.exists_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α} {p : αProp} (hp : ∀ᶠ (x : α) in nhds a, p x) :
            l u, a Set.Ioo l u Set.Ioo l u {x | p x}
            theorem Dense.topology_eq_generateFrom {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) :
            inst✝ = TopologicalSpace.generateFrom (Set.Ioi '' s Set.Iio '' s)

            Let α be a densely ordered linear order with order topology. If α is a separable space, then it has second countable topology. Note that the "densely ordered" assumption cannot be dropped, see double arrow space for a counterexample.

            The set of points which are isolated on the right is countable when the space is second-countable.

            @[deprecated countable_setOf_covby_right]

            The set of points which are isolated on the right is countable when the space is second-countable.

            The set of points which are isolated on the left is countable when the space is second-countable.

            The set of points which are isolated on the left is countable when the space is second-countable.

            theorem Set.PairwiseDisjoint.countable_of_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [TopologicalSpace.SecondCountableTopology α] {y : αα} {s : Set α} (h : Set.PairwiseDisjoint s fun x => Set.Ioo x (y x)) (h' : ∀ (x : α), x sx < y x) :

            Consider a disjoint family of intervals (x, y) with x < y in a second-countable space. Then the family is countable. This is not a straightforward consequence of second-countability as some of these intervals might be empty (but in fact this can happen only for countably many of them).

            Intervals in Π i, π i belong to 𝓝 x #

            For each lemma pi_Ixx_mem_nhds we add a non-dependent version pi_Ixx_mem_nhds' because sometimes Lean fails to unify different instances while trying to apply the dependent version to, e.g., ι → ℝ.

            theorem pi_Iic_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {x : (i : ι) → π i} (ha : ∀ (i : ι), x i < a i) :
            theorem pi_Iic_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {x' : ια} (ha : ∀ (i : ι), x' i < a' i) :
            theorem pi_Ici_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {x : (i : ι) → π i} (ha : ∀ (i : ι), a i < x i) :
            theorem pi_Ici_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {x' : ια} (ha : ∀ (i : ι), a' i < x' i) :
            theorem pi_Icc_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {x : (i : ι) → π i} (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
            theorem pi_Icc_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {b' : ια} {x' : ια} (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
            Set.Icc a' b' nhds x'
            theorem pi_Iio_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), x i < a i) :
            theorem pi_Iio_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {x' : ια} [Nonempty ι] (ha : ∀ (i : ι), x' i < a' i) :
            theorem pi_Ioi_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) :
            theorem pi_Ioi_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {x' : ια} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) :
            theorem pi_Ioc_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
            theorem pi_Ioc_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {b' : ια} {x' : ια} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
            Set.Ioc a' b' nhds x'
            theorem pi_Ico_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
            theorem pi_Ico_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {b' : ια} {x' : ια} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
            Set.Ico a' b' nhds x'
            theorem pi_Ioo_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
            theorem pi_Ioo_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {b' : ια} {x' : ια} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
            Set.Ioo a' b' nhds x'
            theorem disjoint_nhds_atTop {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (x : α) :
            Disjoint (nhds x) Filter.atTop
            @[simp]
            theorem inf_nhds_atTop {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (x : α) :
            nhds x Filter.atTop =
            theorem disjoint_nhds_atBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] (x : α) :
            Disjoint (nhds x) Filter.atBot
            @[simp]
            theorem inf_nhds_atBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] (x : α) :
            nhds x Filter.atBot =
            theorem not_tendsto_nhds_of_tendsto_atTop {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] {F : Filter β} [Filter.NeBot F] {f : βα} (hf : Filter.Tendsto f F Filter.atTop) (x : α) :
            theorem not_tendsto_atTop_of_tendsto_nhds {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] {F : Filter β} [Filter.NeBot F] {f : βα} {x : α} (hf : Filter.Tendsto f F (nhds x)) :
            ¬Filter.Tendsto f F Filter.atTop
            theorem not_tendsto_nhds_of_tendsto_atBot {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] {F : Filter β} [Filter.NeBot F] {f : βα} (hf : Filter.Tendsto f F Filter.atBot) (x : α) :
            theorem not_tendsto_atBot_of_tendsto_nhds {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] {F : Filter β} [Filter.NeBot F] {f : βα} {x : α} (hf : Filter.Tendsto f F (nhds x)) :
            ¬Filter.Tendsto f F Filter.atBot

            Neighborhoods to the left and to the right on an OrderTopology #

            We've seen some properties of left and right neighborhood of a point in an OrderClosedTopology. In an OrderTopology, such neighborhoods can be characterized as the sets containing suitable intervals to the right or to the left of a. We give now these characterizations.

            theorem TFAE_mem_nhdsWithin_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {b : α} (hab : a < b) (s : Set α) :
            List.TFAE [s nhdsWithin a (Set.Ioi a), s nhdsWithin a (Set.Ioc a b), s nhdsWithin a (Set.Ioo a b), u, u Set.Ioc a b Set.Ioo a u s, u, u Set.Ioi a Set.Ioo a u s]

            The following statements are equivalent:

            1. s is a neighborhood of a within (a, +∞);
            2. s is a neighborhood of a within (a, b];
            3. s is a neighborhood of a within (a, b);
            4. s includes (a, u) for some u ∈ (a, b];
            5. s includes (a, u) for some u > a.
            theorem mem_nhdsWithin_Ioi_iff_exists_mem_Ioc_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {u' : α} {s : Set α} (hu' : a < u') :
            s nhdsWithin a (Set.Ioi a) u, u Set.Ioc a u' Set.Ioo a u s
            theorem mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {u' : α} {s : Set α} (hu' : a < u') :
            s nhdsWithin a (Set.Ioi a) u, u Set.Ioi a Set.Ioo a u s

            A set is a neighborhood of a within (a, +∞) if and only if it contains an interval (a, u) with a < u < u', provided a is not a top element.

            theorem nhdsWithin_Ioi_basis' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (h : b, a < b) :
            Filter.HasBasis (nhdsWithin a (Set.Ioi a)) (fun x => a < x) (Set.Ioo a)
            theorem mem_nhdsWithin_Ioi_iff_exists_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] {a : α} {s : Set α} :
            s nhdsWithin a (Set.Ioi a) u, u Set.Ioi a Set.Ioo a u s

            A set is a neighborhood of a within (a, +∞) if and only if it contains an interval (a, u) with a < u.

            The set of points which are isolated on the right is countable when the space is second-countable.

            The set of points which are isolated on the left is countable when the space is second-countable.

            A set is a neighborhood of a within (a, +∞) if and only if it contains an interval (a, u] with a < u.

            theorem TFAE_mem_nhdsWithin_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {b : α} (h : a < b) (s : Set α) :
            List.TFAE [s nhdsWithin b (Set.Iio b), s nhdsWithin b (Set.Ico a b), s nhdsWithin b (Set.Ioo a b), l, l Set.Ico a b Set.Ioo l b s, l, l Set.Iio b Set.Ioo l b s]

            The following statements are equivalent:

            1. s is a neighborhood of b within (-∞, b)
            2. s is a neighborhood of b within [a, b)
            3. s is a neighborhood of b within (a, b)
            4. s includes (l, b) for some l ∈ [a, b)
            5. s includes (l, b) for some l < b
            theorem mem_nhdsWithin_Iio_iff_exists_mem_Ico_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {l' : α} {s : Set α} (hl' : l' < a) :
            s nhdsWithin a (Set.Iio a) l, l Set.Ico l' a Set.Ioo l a s
            theorem mem_nhdsWithin_Iio_iff_exists_Ioo_subset' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {l' : α} {s : Set α} (hl' : l' < a) :
            s nhdsWithin a (Set.Iio a) l, l Set.Iio a Set.Ioo l a s

            A set is a neighborhood of a within (-∞, a) if and only if it contains an interval (l, a) with l < a, provided a is not a bottom element.

            theorem mem_nhdsWithin_Iio_iff_exists_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] {a : α} {s : Set α} :
            s nhdsWithin a (Set.Iio a) l, l Set.Iio a Set.Ioo l a s

            A set is a neighborhood of a within (-∞, a) if and only if it contains an interval (l, a) with l < a.

            A set is a neighborhood of a within (-∞, a) if and only if it contains an interval [l, a) with l < a.

            theorem nhdsWithin_Iio_basis' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (h : b, b < a) :
            Filter.HasBasis (nhdsWithin a (Set.Iio a)) (fun x => x < a) fun x => Set.Ioo x a
            theorem TFAE_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {b : α} (hab : a < b) (s : Set α) :
            List.TFAE [s nhdsWithin a (Set.Ici a), s nhdsWithin a (Set.Icc a b), s nhdsWithin a (Set.Ico a b), u, u Set.Ioc a b Set.Ico a u s, u, u Set.Ioi a Set.Ico a u s]

            The following statements are equivalent:

            1. s is a neighborhood of a within [a, +∞);
            2. s is a neighborhood of a within [a, b];
            3. s is a neighborhood of a within [a, b);
            4. s includes [a, u) for some u ∈ (a, b];
            5. s includes [a, u) for some u > a.
            theorem mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {u' : α} {s : Set α} (hu' : a < u') :
            s nhdsWithin a (Set.Ici a) u, u Set.Ioc a u' Set.Ico a u s
            theorem mem_nhdsWithin_Ici_iff_exists_Ico_subset' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {u' : α} {s : Set α} (hu' : a < u') :
            s nhdsWithin a (Set.Ici a) u, u Set.Ioi a Set.Ico a u s

            A set is a neighborhood of a within [a, +∞) if and only if it contains an interval [a, u) with a < u < u', provided a is not a top element.

            theorem mem_nhdsWithin_Ici_iff_exists_Ico_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] {a : α} {s : Set α} :
            s nhdsWithin a (Set.Ici a) u, u Set.Ioi a Set.Ico a u s

            A set is a neighborhood of a within [a, +∞) if and only if it contains an interval [a, u) with a < u.

            theorem nhdsWithin_Ici_basis_Ico {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) :
            Filter.HasBasis (nhdsWithin a (Set.Ici a)) (fun u => a < u) (Set.Ico a)
            theorem mem_nhdsWithin_Ici_iff_exists_Icc_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] {a : α} {s : Set α} :
            s nhdsWithin a (Set.Ici a) u, a < u Set.Icc a u s

            A set is a neighborhood of a within [a, +∞) if and only if it contains an interval [a, u] with a < u.

            theorem TFAE_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {b : α} (h : a < b) (s : Set α) :
            List.TFAE [s nhdsWithin b (Set.Iic b), s nhdsWithin b (Set.Icc a b), s nhdsWithin b (Set.Ioc a b), l, l Set.Ico a b Set.Ioc l b s, l, l Set.Iio b Set.Ioc l b s]

            The following statements are equivalent:

            1. s is a neighborhood of b within (-∞, b]
            2. s is a neighborhood of b within [a, b]
            3. s is a neighborhood of b within (a, b]
            4. s includes (l, b] for some l ∈ [a, b)
            5. s includes (l, b] for some l < b
            theorem mem_nhdsWithin_Iic_iff_exists_mem_Ico_Ioc_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {l' : α} {s : Set α} (hl' : l' < a) :
            s nhdsWithin a (Set.Iic a) l, l Set.Ico l' a Set.Ioc l a s
            theorem mem_nhdsWithin_Iic_iff_exists_Ioc_subset' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {l' : α} {s : Set α} (hl' : l' < a) :
            s nhdsWithin a (Set.Iic a) l, l Set.Iio a Set.Ioc l a s

            A set is a neighborhood of a within (-∞, a] if and only if it contains an interval (l, a] with l < a, provided a is not a bottom element.

            theorem mem_nhdsWithin_Iic_iff_exists_Ioc_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] {a : α} {s : Set α} :
            s nhdsWithin a (Set.Iic a) l, l Set.Iio a Set.Ioc l a s

            A set is a neighborhood of a within (-∞, a] if and only if it contains an interval (l, a] with l < a.

            theorem mem_nhdsWithin_Iic_iff_exists_Icc_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] [DenselyOrdered α] {a : α} {s : Set α} :
            s nhdsWithin a (Set.Iic a) l, l < a Set.Icc l a s

            A set is a neighborhood of a within (-∞, a] if and only if it contains an interval [l, a] with l < a.

            theorem nhds_eq_iInf_abs_sub {α : Type u} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] (a : α) :
            nhds a = ⨅ (r : α) (_ : r > 0), Filter.principal {b | |a - b| < r}
            theorem orderTopology_of_nhds_abs {α : Type u_1} [TopologicalSpace α] [LinearOrderedAddCommGroup α] (h_nhds : ∀ (a : α), nhds a = ⨅ (r : α) (_ : r > 0), Filter.principal {b | |a - b| < r}) :
            theorem LinearOrderedAddCommGroup.tendsto_nhds {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {f : βα} {x : Filter β} {a : α} :
            Filter.Tendsto f x (nhds a) ∀ (ε : α), ε > 0∀ᶠ (b : β) in x, |f b - a| < ε
            theorem eventually_abs_sub_lt {α : Type u} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] (a : α) {ε : α} (hε : 0 < ε) :
            ∀ᶠ (x : α) in nhds a, |x - a| < ε
            theorem Filter.Tendsto.add_atTop {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {l : Filter β} {f : βα} {g : βα} {C : α} (hf : Filter.Tendsto f l (nhds C)) (hg : Filter.Tendsto g l Filter.atTop) :
            Filter.Tendsto (fun x => f x + g x) l Filter.atTop

            In a linearly ordered additive commutative group with the order topology, if f tends to C and g tends to atTop then f + g tends to atTop.

            theorem Filter.Tendsto.add_atBot {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {l : Filter β} {f : βα} {g : βα} {C : α} (hf : Filter.Tendsto f l (nhds C)) (hg : Filter.Tendsto g l Filter.atBot) :
            Filter.Tendsto (fun x => f x + g x) l Filter.atBot

            In a linearly ordered additive commutative group with the order topology, if f tends to C and g tends to atBot then f + g tends to atBot.

            theorem Filter.Tendsto.atTop_add {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {l : Filter β} {f : βα} {g : βα} {C : α} (hf : Filter.Tendsto f l Filter.atTop) (hg : Filter.Tendsto g l (nhds C)) :
            Filter.Tendsto (fun x => f x + g x) l Filter.atTop

            In a linearly ordered additive commutative group with the order topology, if f tends to atTop and g tends to C then f + g tends to atTop.

            theorem Filter.Tendsto.atBot_add {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] {l : Filter β} {f : βα} {g : βα} {C : α} (hf : Filter.Tendsto f l Filter.atBot) (hg : Filter.Tendsto g l (nhds C)) :
            Filter.Tendsto (fun x => f x + g x) l Filter.atBot

            In a linearly ordered additive commutative group with the order topology, if f tends to atBot and g tends to C then f + g tends to atBot.

            theorem nhds_basis_abs_sub_lt {α : Type u} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] (a : α) :
            Filter.HasBasis (nhds a) (fun ε => 0 < ε) fun ε => {b | |b - a| < ε}
            theorem nhds_basis_Ioo_pos {α : Type u} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] (a : α) :
            Filter.HasBasis (nhds a) (fun ε => 0 < ε) fun ε => Set.Ioo (a - ε) (a + ε)
            theorem nhds_basis_Icc_pos {α : Type u} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] (a : α) :
            Filter.HasBasis (nhds a) (fun x => 0 < x) fun ε => Set.Icc (a - ε) (a + ε)
            theorem nhds_basis_zero_abs_sub_lt (α : Type u) [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] :
            Filter.HasBasis (nhds 0) (fun ε => 0 < ε) fun ε => {b | |b| < ε}
            theorem nhds_basis_Ioo_pos_of_pos {α : Type u} [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] [NoMaxOrder α] {a : α} (ha : 0 < a) :
            Filter.HasBasis (nhds a) (fun ε => 0 < ε ε a) fun ε => Set.Ioo (a - ε) (a + ε)

            If a is positive we can form a basis from only nonnegative Set.Ioo intervals

            @[deprecated Set.image_neg]
            theorem preimage_neg {α : Type u} [AddGroup α] :
            Set.preimage Neg.neg = Set.image Neg.neg
            @[deprecated]
            theorem Filter.map_neg_eq_comap_neg {α : Type u} [AddGroup α] :
            Filter.map Neg.neg = Filter.comap Neg.neg
            theorem IsLUB.frequently_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : Set.Nonempty s) :
            ∃ᶠ (x : α) in nhdsWithin a (Set.Iic a), x s
            theorem IsLUB.frequently_nhds_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : Set.Nonempty s) :
            ∃ᶠ (x : α) in nhds a, x s
            theorem IsGLB.frequently_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsGLB s a) (hs : Set.Nonempty s) :
            ∃ᶠ (x : α) in nhdsWithin a (Set.Ici a), x s
            theorem IsGLB.frequently_nhds_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsGLB s a) (hs : Set.Nonempty s) :
            ∃ᶠ (x : α) in nhds a, x s
            theorem IsLUB.mem_closure {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : Set.Nonempty s) :
            theorem IsGLB.mem_closure {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsGLB s a) (hs : Set.Nonempty s) :
            theorem IsLUB.nhdsWithin_neBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : Set.Nonempty s) :
            theorem IsGLB.nhdsWithin_neBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} :
            theorem isLUB_of_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {s : Set α} {a : α} {f : Filter α} (hsa : a upperBounds s) (hsf : s f) [Filter.NeBot (f nhds a)] :
            IsLUB s a
            theorem isLUB_of_mem_closure {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {s : Set α} {a : α} (hsa : a upperBounds s) (hsf : a closure s) :
            IsLUB s a
            theorem isGLB_of_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {s : Set α} {a : α} {f : Filter α} :
            a lowerBounds ss fFilter.NeBot (f nhds a)IsGLB s a
            theorem isGLB_of_mem_closure {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {s : Set α} {a : α} (hsa : a lowerBounds s) (hsf : a closure s) :
            IsGLB s a
            theorem IsLUB.mem_upperBounds_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : αγ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) :
            theorem IsLUB.isLUB_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : αγ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a) (hs : Set.Nonempty s) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) :
            IsLUB (f '' s) b
            theorem IsGLB.mem_lowerBounds_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : αγ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsGLB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) :
            theorem IsGLB.isGLB_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : αγ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) :
            IsGLB s aSet.Nonempty sFilter.Tendsto f (nhdsWithin a s) (nhds b)IsGLB (f '' s) b
            theorem IsLUB.mem_lowerBounds_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : αγ} {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s) (ha : IsLUB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) :
            theorem IsLUB.isGLB_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : αγ} {s : Set α} {a : α} {b : γ} :
            AntitoneOn f sIsLUB s aSet.Nonempty sFilter.Tendsto f (nhdsWithin a s) (nhds b)IsGLB (f '' s) b
            theorem IsGLB.mem_upperBounds_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : αγ} {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s) (ha : IsGLB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) :
            theorem IsGLB.isLUB_of_tendsto {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : αγ} {s : Set α} {a : α} {b : γ} :
            AntitoneOn f sIsGLB s aSet.Nonempty sFilter.Tendsto f (nhdsWithin a s) (nhds b)IsLUB (f '' s) b
            theorem IsLUB.mem_of_isClosed {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : Set.Nonempty s) (sc : IsClosed s) :
            a s
            theorem IsClosed.isLUB_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : Set.Nonempty s) (sc : IsClosed s) :
            a s

            Alias of IsLUB.mem_of_isClosed.

            theorem IsGLB.mem_of_isClosed {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsGLB s a) (hs : Set.Nonempty s) (sc : IsClosed s) :
            a s
            theorem IsClosed.isGLB_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsGLB s a) (hs : Set.Nonempty s) (sc : IsClosed s) :
            a s

            Alias of IsGLB.mem_of_isClosed.

            Existence of sequences tending to sInf or sSup of a given set #

            theorem IsLUB.exists_seq_strictMono_tendsto_of_not_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α} {x : α} [Filter.IsCountablyGenerated (nhds x)] (htx : IsLUB t x) (not_mem : ¬x t) (ht : Set.Nonempty t) :
            u, StrictMono u (∀ (n : ), u n < x) Filter.Tendsto u Filter.atTop (nhds x) ∀ (n : ), u n t
            theorem IsLUB.exists_seq_monotone_tendsto {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α} {x : α} [Filter.IsCountablyGenerated (nhds x)] (htx : IsLUB t x) (ht : Set.Nonempty t) :
            u, Monotone u (∀ (n : ), u n x) Filter.Tendsto u Filter.atTop (nhds x) ∀ (n : ), u n t
            theorem exists_seq_strictMono_tendsto' {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [DenselyOrdered α] [OrderTopology α] [TopologicalSpace.FirstCountableTopology α] {x : α} {y : α} (hy : y < x) :
            u, StrictMono u (∀ (n : ), u n Set.Ioo y x) Filter.Tendsto u Filter.atTop (nhds x)
            theorem IsGLB.exists_seq_strictAnti_tendsto_of_not_mem {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α} {x : α} [Filter.IsCountablyGenerated (nhds x)] (htx : IsGLB t x) (not_mem : ¬x t) (ht : Set.Nonempty t) :
            u, StrictAnti u (∀ (n : ), x < u n) Filter.Tendsto u Filter.atTop (nhds x) ∀ (n : ), u n t
            theorem IsGLB.exists_seq_antitone_tendsto {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α} {x : α} [Filter.IsCountablyGenerated (nhds x)] (htx : IsGLB t x) (ht : Set.Nonempty t) :
            u, Antitone u (∀ (n : ), x u n) Filter.Tendsto u Filter.atTop (nhds x) ∀ (n : ), u n t
            theorem exists_seq_strictAnti_tendsto' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [TopologicalSpace.FirstCountableTopology α] {x : α} {y : α} (hy : x < y) :
            u, StrictAnti u (∀ (n : ), u n Set.Ioo x y) Filter.Tendsto u Filter.atTop (nhds x)
            theorem exists_seq_strictAnti_strictMono_tendsto {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [TopologicalSpace.FirstCountableTopology α] {x : α} {y : α} (h : x < y) :
            u v, StrictAnti u StrictMono v (∀ (k : ), u k Set.Ioo x y) (∀ (l : ), v l Set.Ioo x y) (∀ (k l : ), u k < v l) Filter.Tendsto u Filter.atTop (nhds x) Filter.Tendsto v Filter.atTop (nhds y)
            theorem closure_Ioi' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (h : Set.Nonempty (Set.Ioi a)) :

            The closure of the interval (a, +∞) is the closed interval [a, +∞), unless a is a top element.

            @[simp]
            theorem closure_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) [NoMaxOrder α] :

            The closure of the interval (a, +∞) is the closed interval [a, +∞).

            theorem closure_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (h : Set.Nonempty (Set.Iio a)) :

            The closure of the interval (-∞, a) is the closed interval (-∞, a], unless a is a bottom element.

            @[simp]
            theorem closure_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α) [NoMinOrder α] :

            The closure of the interval (-∞, a) is the interval (-∞, a].

            @[simp]
            theorem closure_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (hab : a b) :

            The closure of the open interval (a, b) is the closed interval [a, b].

            @[simp]
            theorem closure_Ioc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (hab : a b) :

            The closure of the interval (a, b] is the closed interval [a, b].

            @[simp]
            theorem closure_Ico {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (hab : a b) :

            The closure of the interval [a, b) is the closed interval [a, b].

            @[simp]
            @[simp]
            @[simp]
            theorem interior_Icc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] {a : α} {b : α} :
            @[simp]
            theorem interior_Ico {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} {b : α} :
            @[simp]
            theorem interior_Ioc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} {b : α} :
            theorem closure_interior_Icc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (h : a b) :
            @[simp]
            theorem frontier_Ici' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : Set.Nonempty (Set.Iio a)) :
            theorem frontier_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} :
            @[simp]
            theorem frontier_Iic' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : Set.Nonempty (Set.Ioi a)) :
            theorem frontier_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} :
            @[simp]
            theorem frontier_Ioi' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : Set.Nonempty (Set.Ioi a)) :
            theorem frontier_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} :
            @[simp]
            theorem frontier_Iio' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : Set.Nonempty (Set.Iio a)) :
            theorem frontier_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} :
            @[simp]
            theorem frontier_Icc {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] {a : α} {b : α} (h : a b) :
            frontier (Set.Icc a b) = {a, b}
            @[simp]
            theorem frontier_Ioo {α : Type u} [