Documentation

Mathlib.Topology.Order.OrderClosed

Order-closed topologies #

In this file we introduce 3 typeclass mixins that relate topology and order structures:

The last predicate implies the first two.

We prove many basic properties of such topologies.

Main statements #

This file contains the proofs of the following facts. For exact requirements (OrderClosedTopology vs ClosedIciTopoplogy vs ClosedIicTopology, PreordervsPartialOrdervsLinearOrder` etc) see their statements.

Open / closed sets #

Convergence and inequalities #

Min, max, sSup and sInf #

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

  • isClosed_Iic : ∀ (a : α), IsClosed (Set.Iic a)

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

Instances

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

    • isClosed_Ici : ∀ (a : α), IsClosed (Set.Ici a)

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

    Instances

      A topology on a set which is both a topological space and a preorder is order-closed if the set of points (x, y) with x ≤ y is closed in the product space. We introduce this as a mixin. This property is satisfied for the order topology on a linear order, but it can be satisfied more generally, and suffices to derive many interesting properties relating order and topology.

      • isClosed_le' : IsClosed {p : α × α | p.1 p.2}

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

      Instances
        theorem Dense.orderDual {α : Type u} [TopologicalSpace α] {s : Set α} (hs : Dense s) :
        Dense (OrderDual.ofDual ⁻¹' s)
        theorem BddAbove.of_closure {α : Type u} [TopologicalSpace α] [Preorder α] {s : Set α} :
        theorem BddBelow.of_closure {α : Type u} [TopologicalSpace α] [Preorder α] {s : Set α} :
        theorem isClosed_Iic {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {a : α} :
        @[deprecated ClosedIicTopology.isClosed_Iic]
        theorem ClosedIicTopology.isClosed_le' {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] (a : α) :
        IsClosed {x : α | x a}
        @[simp]
        theorem closure_Iic {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] (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 BddAbove.closure {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s : Set α} :

        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)) :
        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 : α) :
        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 : α} :
        @[simp]
        theorem interior_Ioi {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} :
        theorem Ioi_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (h : a < 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) :
        theorem eventually_ge_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (hab : b < a) :
        ∀ᶠ (x : α) in nhds a, b x
        theorem Filter.Tendsto.eventually_const_lt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {l : Filter γ} {f : γα} {u v : α} (hv : u < v) (h : Filter.Tendsto f l (nhds v)) :
        ∀ᶠ (a : γ) in l, u < f a
        @[deprecated Filter.Tendsto.eventually_const_lt]
        theorem eventually_gt_of_tendsto_gt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {l : Filter γ} {f : γα} {u v : α} (hv : u < v) (h : Filter.Tendsto f l (nhds v)) :
        ∀ᶠ (a : γ) in l, u < f a

        Alias of Filter.Tendsto.eventually_const_lt.

        theorem Filter.Tendsto.eventually_const_le {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {l : Filter γ} {f : γα} {u v : α} (hv : u < v) (h : Filter.Tendsto f l (nhds v)) :
        ∀ᶠ (a : γ) in l, u f a
        @[deprecated Filter.Tendsto.eventually_const_le]
        theorem eventually_ge_of_tendsto_gt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {l : Filter γ} {f : γα} {u v : α} (hv : u < v) (h : Filter.Tendsto f l (nhds v)) :
        ∀ᶠ (a : γ) in l, u f a

        Alias of Filter.Tendsto.eventually_const_le.

        theorem Dense.exists_gt {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) :
        ys, x < y
        theorem Dense.exists_ge {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) :
        ys, x y
        theorem Dense.exists_ge' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {s : Set α} (hs : Dense s) (htop : ∀ (x : α), IsTop xx s) (x : α) :
        ys, x y

        Left neighborhoods on a ClosedIicTopology #

        Limits to the left of real functions are defined in terms of neighborhoods to the left, either open or closed, i.e., members of 𝓝[<] a and 𝓝[≤] a. Here we prove that all left-neighborhoods of a point are equal, and we prove other useful characterizations which require the stronger hypothesis OrderTopology α in another file.

        Point excluded #

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

        Point included #

        theorem CovBy.nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a b) :
        theorem Ioc_mem_nhdsWithin_Iic' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) :
        theorem Ioo_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b c : α} (H : b Set.Ioo a c) :
        theorem Ico_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b c : α} (H : b Set.Ioo a c) :
        theorem Ioc_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b c : α} (H : b Set.Ioc a c) :
        theorem Icc_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b c : α} (H : b Set.Ioc a c) :
        theorem Icc_mem_nhdsWithin_Iic' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) :
        @[simp]
        theorem nhdsWithin_Icc_eq_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (h : a < b) :
        @[simp]
        theorem nhdsWithin_Ioc_eq_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (h : a < b) :
        @[simp]
        theorem continuousWithinAt_Icc_iff_Iic {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [TopologicalSpace β] {a b : α} {f : αβ} (h : a < b) :
        @[simp]
        theorem continuousWithinAt_Ioc_iff_Iic {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [TopologicalSpace β] {a b : α} {f : αβ} (h : a < b) :
        theorem isClosed_Ici {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {a : α} :
        @[deprecated]
        theorem ClosedIciTopology.isClosed_ge' {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] (a : α) :
        IsClosed {x : α | a x}
        @[simp]
        theorem closure_Ici {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] (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 BddBelow.closure {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {s : Set α} :

        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)) :
        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 : α) :
        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 : α} :
        @[simp]
        theorem interior_Iio {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a : α} :
        theorem Iio_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (h : a < b) :
        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) :
        theorem eventually_le_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (hab : a < b) :
        ∀ᶠ (x : α) in nhds a, x b
        theorem Filter.Tendsto.eventually_lt_const {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {l : Filter γ} {f : γα} {u v : α} (hv : v < u) (h : Filter.Tendsto f l (nhds v)) :
        ∀ᶠ (a : γ) in l, f a < u
        @[deprecated Filter.Tendsto.eventually_lt_const]
        theorem eventually_lt_of_tendsto_lt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {l : Filter γ} {f : γα} {u v : α} (hv : v < u) (h : Filter.Tendsto f l (nhds v)) :
        ∀ᶠ (a : γ) in l, f a < u

        Alias of Filter.Tendsto.eventually_lt_const.

        theorem Filter.Tendsto.eventually_le_const {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {l : Filter γ} {f : γα} {u v : α} (hv : v < u) (h : Filter.Tendsto f l (nhds v)) :
        ∀ᶠ (a : γ) in l, f a u
        @[deprecated Filter.Tendsto.eventually_le_const]
        theorem eventually_le_of_tendsto_lt {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {l : Filter γ} {f : γα} {u v : α} (hv : v < u) (h : Filter.Tendsto f l (nhds v)) :
        ∀ᶠ (a : γ) in l, f a u

        Alias of Filter.Tendsto.eventually_le_const.

        theorem Dense.exists_lt {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) :
        ys, y < x
        theorem Dense.exists_le {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) :
        ys, y x
        theorem Dense.exists_le' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {s : Set α} (hs : Dense s) (hbot : ∀ (x : α), IsBot xx s) (x : α) :
        ys, y x

        Right neighborhoods on a ClosedIciTopology #

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

        Point excluded #

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

        Point included #

        theorem CovBy.nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (H : a b) :
        theorem Ico_mem_nhdsWithin_Ici' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (H : a < b) :
        theorem Ico_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b c : α} (H : b Set.Ico a c) :
        theorem Ioo_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b c : α} (H : b Set.Ioo a c) :
        theorem Ioc_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b c : α} (H : b Set.Ioo a c) :
        theorem Icc_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b c : α} (H : b Set.Ico a c) :
        theorem Icc_mem_nhdsWithin_Ici' {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (H : a < b) :
        @[simp]
        theorem nhdsWithin_Icc_eq_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (h : a < b) :
        @[simp]
        theorem nhdsWithin_Ico_eq_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (h : a < b) :
        @[simp]
        theorem continuousWithinAt_Icc_iff_Ici {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [TopologicalSpace β] {a b : α} {f : αβ} (h : a < b) :
        @[simp]
        theorem continuousWithinAt_Ico_iff_Ici {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [TopologicalSpace β] {a b : α} {f : αβ} (h : a < b) :
        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}
        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₂ : α} [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 : ys, 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 : xs, 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}
        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 : α} :
        @[simp]
        theorem interior_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {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) :

        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_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 : β) => 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) :
        zs, 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 = ys 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 = ys Set.Iio x, Set.Iio y
        theorem instOrderClosedTopologyForall {ι : Type u_1} {α : ιType u_2} [(i : ι) → Preorder (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OrderClosedTopology (α i)] :
        OrderClosedTopology ((i : ι) → α i)