Mathlib.Topology.Order.Monotone

sSup_mem_closure theorem

{s : Set α} (hs : s.Nonempty) : sSup s ∈ closure s

Full source

theorem sSup_mem_closure {s : Set α} (hs : s.Nonempty) : sSupsSup s ∈ closure s :=
  (isLUB_sSup s).mem_closure hs

Supremum Belongs to Closure of Nonempty Set

Informal description

For any nonempty subset $s$ of a topological space $\alpha$ with a conditionally complete linear order, the supremum of $s$ belongs to the closure of $s$.

sInf_mem_closure theorem

{s : Set α} (hs : s.Nonempty) : sInf s ∈ closure s

Full source

theorem sInf_mem_closure {s : Set α} (hs : s.Nonempty) : sInfsInf s ∈ closure s :=
  (isGLB_sInf s).mem_closure hs

Infimum of Nonempty Set Belongs to its Closure

Informal description

For any nonempty subset $s$ of a conditionally complete linear order $\alpha$, the infimum of $s$ belongs to the topological closure of $s$.

IsClosed.sSup_mem theorem

{s : Set α} (hs : s.Nonempty) (hc : IsClosed s) : sSup s ∈ s

Full source

theorem IsClosed.sSup_mem {s : Set α} (hs : s.Nonempty) (hc : IsClosed s) : sSupsSup s ∈ s :=
  (isLUB_sSup s).mem_of_isClosed hs hc

Closed Sets Contain Their Supremum

Informal description

For any nonempty subset $s$ of a topological space $\alpha$ with a conditionally complete linear order, if $s$ is closed, then its supremum $\sup s$ belongs to $s$.

IsClosed.sInf_mem theorem

{s : Set α} (hs : s.Nonempty) (hc : IsClosed s) : sInf s ∈ s

Full source

theorem IsClosed.sInf_mem {s : Set α} (hs : s.Nonempty) (hc : IsClosed s) : sInfsInf s ∈ s :=
  (isGLB_sInf s).mem_of_isClosed hs hc

Closed Nonempty Sets Contain Their Infimum in Complete Linear Orders

Informal description

For any nonempty subset $s$ of a complete linear order $\alpha$, if $s$ is closed in the order topology, then the infimum of $s$ belongs to $s$.

MonotoneOn.map_sSup_of_continuousWithinAt theorem

 {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sSup s)) (Mf : MonotoneOn f s) (fbot : f ⊥ = ⊥) :
  f (sSup s) = sSup (f '' s)

Full source

/-- A monotone function `f` sending `bot` to `bot` and continuous at the supremum of a set sends
this supremum to the supremum of the image of this set. -/
theorem MonotoneOn.map_sSup_of_continuousWithinAt {f : α → β} {s : Set α}
    (Cf : ContinuousWithinAt f s (sSup s))
    (Mf : MonotoneOn f s) (fbot : f ⊥ = ⊥) : f (sSup s) = sSup (f '' s) := by
  rcases s.eq_empty_or_nonempty with h | h
  · simp [h, fbot]
  · exact Mf.map_csSup_of_continuousWithinAt Cf h

Supremum Preservation Under Monotone Continuous Functions

Informal description

Let $f : \alpha \to \beta$ be a function defined on a subset $s$ of a complete linear order $\alpha$ with bottom element $\bot$. If: 1. $f$ is continuous within $s$ at $\sup s$, 2. $f$ is monotone on $s$, and 3. $f(\bot) = \bot$, then $f(\sup s) = \sup (f '' s)$, where $f '' s$ denotes the image of $s$ under $f$.

Monotone.map_sSup_of_continuousAt theorem

 {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Mf : Monotone f) (fbot : f ⊥ = ⊥) : f (sSup s) = sSup (f '' s)

Full source

/-- A monotone function `f` sending `bot` to `bot` and continuous at the supremum of a set sends
this supremum to the supremum of the image of this set. -/
theorem Monotone.map_sSup_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s))
    (Mf : Monotone f) (fbot : f ⊥ = ⊥) : f (sSup s) = sSup (f '' s) :=
  MonotoneOn.map_sSup_of_continuousWithinAt Cf.continuousWithinAt (Mf.monotoneOn _) fbot

Supremum Preservation Under Monotone Continuous Functions at Supremum Point

Informal description

Let $f : \alpha \to \beta$ be a monotone function between complete linear orders with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively, such that $f(\bot_\alpha) = \bot_\beta$. If $f$ is continuous at $\sup s$ for some subset $s \subseteq \alpha$, then $f(\sup s) = \sup (f(s))$.

Monotone.map_iSup_of_continuousAt theorem

 {ι : Sort*} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Mf : Monotone f) (fbot : f ⊥ = ⊥) :
  f (⨆ i, g i) = ⨆ i, f (g i)

Full source

/-- If a monotone function sending `bot` to `bot` is continuous at the indexed supremum over
a `Sort`, then it sends this indexed supremum to the indexed supremum of the composition. -/
theorem Monotone.map_iSup_of_continuousAt {ι : Sort*} {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iSup g)) (Mf : Monotone f) (fbot : f ⊥ = ⊥) :
    f (⨆ i, g i) = ⨆ i, f (g i) := by
  rw [iSup, Mf.map_sSup_of_continuousAt Cf fbot, ← range_comp, iSup, comp_def]

Supremum Preservation Under Monotone Continuous Functions for Indexed Families

Informal description

Let $\alpha$ and $\beta$ be complete linear orders with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively. Given a monotone function $f : \alpha \to \beta$ such that $f(\bot_\alpha) = \bot_\beta$ and a family of elements $(g_i)_{i \in \iota}$ in $\alpha$, if $f$ is continuous at $\sup_{i \in \iota} g_i$, then $f(\sup_{i \in \iota} g_i) = \sup_{i \in \iota} f(g_i)$.

MonotoneOn.map_sInf_of_continuousWithinAt theorem

 {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sInf s)) (Mf : MonotoneOn f s) (ftop : f ⊤ = ⊤) :
  f (sInf s) = sInf (f '' s)

Full source

/-- A monotone function `f` sending `top` to `top` and continuous at the infimum of a set sends
this infimum to the infimum of the image of this set. -/
theorem MonotoneOn.map_sInf_of_continuousWithinAt {f : α → β} {s : Set α}
    (Cf : ContinuousWithinAt f s (sInf s)) (Mf : MonotoneOn f s) (ftop : f ⊤ = ⊤) :
    f (sInf s) = sInf (f '' s) :=
  MonotoneOn.map_sSup_of_continuousWithinAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual ftop

Infimum Preservation Under Monotone Continuous Functions with Top Condition

Informal description

Let $f : \alpha \to \beta$ be a function defined on a subset $s$ of a complete linear order $\alpha$ with top element $\top$. If: 1. $f$ is continuous within $s$ at $\inf s$, 2. $f$ is monotone on $s$, and 3. $f(\top) = \top$, then $f(\inf s) = \inf (f '' s)$, where $f '' s$ denotes the image of $s$ under $f$.

Monotone.map_sInf_of_continuousAt theorem

 {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Mf : Monotone f) (ftop : f ⊤ = ⊤) : f (sInf s) = sInf (f '' s)

Full source

/-- A monotone function `f` sending `top` to `top` and continuous at the infimum of a set sends
this infimum to the infimum of the image of this set. -/
theorem Monotone.map_sInf_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s))
    (Mf : Monotone f) (ftop : f ⊤ = ⊤) : f (sInf s) = sInf (f '' s) :=
  Monotone.map_sSup_of_continuousAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual ftop

Infimum Preservation Under Monotone Continuous Functions at Infimum Point with Top Condition

Informal description

Let $f : \alpha \to \beta$ be a monotone function between complete linear orders with top elements $\top_\alpha$ and $\top_\beta$ respectively, such that $f(\top_\alpha) = \top_\beta$. If $f$ is continuous at $\inf s$ for some subset $s \subseteq \alpha$, then $f(\inf s) = \inf (f(s))$.

Monotone.map_iInf_of_continuousAt theorem

 {ι : Sort*} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Mf : Monotone f) (ftop : f ⊤ = ⊤) :
  f (iInf g) = iInf (f ∘ g)

Full source

/-- If a monotone function sending `top` to `top` is continuous at the indexed infimum over
a `Sort`, then it sends this indexed infimum to the indexed infimum of the composition. -/
theorem Monotone.map_iInf_of_continuousAt {ι : Sort*} {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iInf g)) (Mf : Monotone f) (ftop : f ⊤ = ⊤) : f (iInf g) = iInf (f ∘ g) :=
  Monotone.map_iSup_of_continuousAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual ftop

Infimum Preservation Under Monotone Continuous Functions for Indexed Families with Top Condition

Informal description

Let $\alpha$ and $\beta$ be complete linear orders with top elements $\top_\alpha$ and $\top_\beta$ respectively. Given a monotone function $f : \alpha \to \beta$ such that $f(\top_\alpha) = \top_\beta$ and a family of elements $(g_i)_{i \in \iota}$ in $\alpha$, if $f$ is continuous at $\inf_{i \in \iota} g_i$, then $f(\inf_{i \in \iota} g_i) = \inf_{i \in \iota} f(g_i)$.

AntitoneOn.map_sSup_of_continuousWithinAt theorem

 {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sSup s)) (Af : AntitoneOn f s) (fbot : f ⊥ = ⊤) :
  f (sSup s) = sInf (f '' s)

Full source

/-- An antitone function `f` sending `bot` to `top` and continuous at the supremum of a set sends
this supremum to the infimum of the image of this set. -/
theorem AntitoneOn.map_sSup_of_continuousWithinAt {f : α → β} {s : Set α}
    (Cf : ContinuousWithinAt f s (sSup s)) (Af : AntitoneOn f s) (fbot : f ⊥ = ⊤) :
    f (sSup s) = sInf (f '' s) :=
  MonotoneOn.map_sSup_of_continuousWithinAt
    (show ContinuousWithinAt (OrderDual.toDualOrderDual.toDual ∘ f) s (sSup s) from Cf) Af fbot

Infimum of Image Under Antitone Continuous Function at Supremum

Informal description

Let $f : \alpha \to \beta$ be an antitone function defined on a subset $s$ of a complete linear order $\alpha$ with bottom element $\bot$. If: 1. $f$ is continuous within $s$ at $\sup s$, 2. $f$ is antitone on $s$, and 3. $f(\bot) = \top$, then $f(\sup s) = \inf (f '' s)$, where $f '' s$ denotes the image of $s$ under $f$.

Antitone.map_sSup_of_continuousAt theorem

 {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Af : Antitone f) (fbot : f ⊥ = ⊤) : f (sSup s) = sInf (f '' s)

Full source

/-- An antitone function `f` sending `bot` to `top` and continuous at the supremum of a set sends
this supremum to the infimum of the image of this set. -/
theorem Antitone.map_sSup_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s))
    (Af : Antitone f) (fbot : f ⊥ = ⊤) : f (sSup s) = sInf (f '' s) :=
  Monotone.map_sSup_of_continuousAt (show ContinuousAt (OrderDual.toDualOrderDual.toDual ∘ f) (sSup s) from Cf) Af
    fbot

Infimum of Image Under Antitone Continuous Function at Supremum

Informal description

Let $f : \alpha \to \beta$ be an antitone function between complete linear orders with bottom elements $\bot_\alpha$ and $\top_\beta$ respectively, such that $f(\bot_\alpha) = \top_\beta$. If $f$ is continuous at $\sup s$ for some subset $s \subseteq \alpha$, then $f(\sup s) = \inf (f(s))$.

Antitone.map_iSup_of_continuousAt theorem

 {ι : Sort*} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Af : Antitone f) (fbot : f ⊥ = ⊤) :
  f (⨆ i, g i) = ⨅ i, f (g i)

Full source

/-- An antitone function sending `bot` to `top` is continuous at the indexed supremum over
a `Sort`, then it sends this indexed supremum to the indexed supremum of the composition. -/
theorem Antitone.map_iSup_of_continuousAt {ι : Sort*} {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iSup g)) (Af : Antitone f) (fbot : f ⊥ = ⊤) :
    f (⨆ i, g i) = ⨅ i, f (g i) :=
  Monotone.map_iSup_of_continuousAt (show ContinuousAt (OrderDual.toDualOrderDual.toDual ∘ f) (iSup g) from Cf) Af
    fbot

Infimum of Image Under Antitone Continuous Function at Indexed Supremum

Informal description

Let $\alpha$ and $\beta$ be complete linear orders with bottom elements $\bot_\alpha$ and $\top_\beta$ respectively. Given an antitone function $f \colon \alpha \to \beta$ such that $f(\bot_\alpha) = \top_\beta$ and a family of elements $(g_i)_{i \in \iota}$ in $\alpha$, if $f$ is continuous at $\sup_{i \in \iota} g_i$, then \[ f\left(\sup_{i \in \iota} g_i\right) = \inf_{i \in \iota} f(g_i). \]

AntitoneOn.map_sInf_of_continuousWithinAt theorem

 {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sInf s)) (Af : AntitoneOn f s) (ftop : f ⊤ = ⊥) :
  f (sInf s) = sSup (f '' s)

Full source

/-- An antitone function `f` sending `top` to `bot` and continuous at the infimum of a set sends
this infimum to the supremum of the image of this set. -/
theorem AntitoneOn.map_sInf_of_continuousWithinAt {f : α → β} {s : Set α}
    (Cf : ContinuousWithinAt f s (sInf s)) (Af : AntitoneOn f s) (ftop : f ⊤ = ⊥) :
    f (sInf s) = sSup (f '' s) :=
  MonotoneOn.map_sInf_of_continuousWithinAt
    (show ContinuousWithinAt (OrderDual.toDualOrderDual.toDual ∘ f) s (sInf s) from Cf) Af ftop

Antitone Function Maps Infimum to Supremum Under Continuity and Top Condition

Informal description

Let $f : \alpha \to \beta$ be an antitone function defined on a subset $s$ of a complete linear order $\alpha$ with top element $\top$. If: 1. $f$ is continuous within $s$ at $\inf s$, 2. $f$ is antitone on $s$, and 3. $f(\top) = \bot$, then $f(\inf s) = \sup (f '' s)$, where $f '' s$ denotes the image of $s$ under $f$.

Antitone.map_sInf_of_continuousAt theorem

 {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Af : Antitone f) (ftop : f ⊤ = ⊥) : f (sInf s) = sSup (f '' s)

Full source

/-- An antitone function `f` sending `top` to `bot` and continuous at the infimum of a set sends
this infimum to the supremum of the image of this set. -/
theorem Antitone.map_sInf_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s))
    (Af : Antitone f) (ftop : f ⊤ = ⊥) : f (sInf s) = sSup (f '' s) :=
  Monotone.map_sInf_of_continuousAt (show ContinuousAt (OrderDual.toDualOrderDual.toDual ∘ f) (sInf s) from Cf) Af
    ftop

Antitone Function Maps Infimum to Supremum Under Continuity and Top-to-Bottom Condition

Informal description

Let $\alpha$ and $\beta$ be complete linear orders, and let $f : \alpha \to \beta$ be an antitone function such that $f(\top_\alpha) = \bot_\beta$. If $f$ is continuous at $\inf s$ for some subset $s \subseteq \alpha$, then $f(\inf s) = \sup (f(s))$, where $f(s)$ denotes the image of $s$ under $f$.

Antitone.map_iInf_of_continuousAt theorem

 {ι : Sort*} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Af : Antitone f) (ftop : f ⊤ = ⊥) :
  f (iInf g) = iSup (f ∘ g)

Full source

/-- If an antitone function sending `top` to `bot` is continuous at the indexed infimum over
a `Sort`, then it sends this indexed infimum to the indexed supremum of the composition. -/
theorem Antitone.map_iInf_of_continuousAt {ι : Sort*} {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iInf g)) (Af : Antitone f) (ftop : f ⊤ = ⊥) : f (iInf g) = iSup (f ∘ g) :=
  Monotone.map_iInf_of_continuousAt (show ContinuousAt (OrderDual.toDualOrderDual.toDual ∘ f) (iInf g) from Cf) Af
    ftop

Antitone Function Maps Infimum to Supremum Under Continuity and Top-to-Bottom Condition for Indexed Families

Informal description

Let $\alpha$ and $\beta$ be complete linear orders with top elements $\top_\alpha$ and $\bot_\beta$ respectively. Given an antitone function $f \colon \alpha \to \beta$ such that $f(\top_\alpha) = \bot_\beta$ and a family of elements $(g_i)_{i \in \iota}$ in $\alpha$, if $f$ is continuous at $\inf_{i \in \iota} g_i$, then $f(\inf_{i \in \iota} g_i) = \sup_{i \in \iota} f(g_i)$.

csSup_mem_closure theorem

{s : Set α} (hs : s.Nonempty) (B : BddAbove s) : sSup s ∈ closure s

Full source

theorem csSup_mem_closure {s : Set α} (hs : s.Nonempty) (B : BddAbove s) : sSupsSup s ∈ closure s :=
  (isLUB_csSup hs B).mem_closure hs

Supremum of Bounded Nonempty Set Belongs to Its Closure

Informal description

Let $\alpha$ be a conditionally complete linear order and $s$ a nonempty subset of $\alpha$ that is bounded above. Then the supremum $\sup s$ belongs to the topological closure of $s$.

csInf_mem_closure theorem

{s : Set α} (hs : s.Nonempty) (B : BddBelow s) : sInf s ∈ closure s

Full source

theorem csInf_mem_closure {s : Set α} (hs : s.Nonempty) (B : BddBelow s) : sInfsInf s ∈ closure s :=
  (isGLB_csInf hs B).mem_closure hs

Infimum lies in closure of bounded-below nonempty set

Informal description

Let $\alpha$ be a conditionally complete linear order and $s$ a nonempty subset of $\alpha$ that is bounded below. Then the infimum $\inf s$ belongs to the topological closure of $s$.

IsClosed.csSup_mem theorem

{s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddAbove s) : sSup s ∈ s

Full source

theorem IsClosed.csSup_mem {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddAbove s) :
    sSupsSup s ∈ s :=
  (isLUB_csSup hs B).mem_of_isClosed hs hc

Supremum of Closed Bounded Nonempty Set Belongs to the Set

Informal description

Let $\alpha$ be a conditionally complete linear order and $s$ a nonempty subset of $\alpha$ that is bounded above. If $s$ is closed, then its supremum $\sup s$ belongs to $s$.

IsClosed.csInf_mem theorem

{s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddBelow s) : sInf s ∈ s

Full source

theorem IsClosed.csInf_mem {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddBelow s) :
    sInfsInf s ∈ s :=
  (isGLB_csInf hs B).mem_of_isClosed hs hc

Infimum of Closed Bounded-Below Set Belongs to Set

Informal description

Let $\alpha$ be a conditionally complete linear order, and let $s$ be a nonempty subset of $\alpha$ that is closed and bounded below. Then the infimum $\inf s$ is an element of $s$.

IsClosed.isLeast_csInf theorem

{s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddBelow s) : IsLeast s (sInf s)

Full source

theorem IsClosed.isLeast_csInf {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddBelow s) :
    IsLeast s (sInf s) :=
  ⟨hc.csInf_mem hs B, (isGLB_csInf hs B).1⟩

Infimum is Least Element in Closed Bounded-Below Sets

Informal description

Let $\alpha$ be a conditionally complete linear order, and let $s$ be a nonempty subset of $\alpha$ that is closed and bounded below. Then the infimum $\inf s$ is the least element of $s$, meaning: 1. $\inf s \in s$, and 2. $\inf s \leq b$ for all $b \in s$.

IsClosed.isGreatest_csSup theorem

{s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddAbove s) : IsGreatest s (sSup s)

Full source

theorem IsClosed.isGreatest_csSup {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddAbove s) :
    IsGreatest s (sSup s) :=
  IsClosed.isLeast_csInf (α := αᵒᵈ) hc hs B

Supremum is Greatest Element in Closed Bounded-Above Sets

Informal description

Let $\alpha$ be a conditionally complete linear order, and let $s$ be a nonempty subset of $\alpha$ that is closed and bounded above. Then the supremum $\sup s$ is the greatest element of $s$, meaning: 1. $\sup s \in s$, and 2. $b \leq \sup s$ for all $b \in s$.

MonotoneOn.tendsto_nhdsWithin_Ioo_left theorem

 {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β]
  [TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α} (h_nonempty : (Ioo y x).Nonempty)
  (Mf : MonotoneOn f (Ioo y x)) (h_bdd : BddAbove (f '' Ioo y x)) : Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Ioo y x)))

Full source

lemma MonotoneOn.tendsto_nhdsWithin_Ioo_left {α β : Type*} [LinearOrder α] [TopologicalSpace α]
    [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β]
    {f : α → β} {x y : α} (h_nonempty : (Ioo y x).Nonempty) (Mf : MonotoneOn f (Ioo y x))
    (h_bdd : BddAbove (f '' Ioo y x)) :
    Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Ioo y x))) := by
  refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩
  · obtain ⟨z, ⟨yz, zx⟩, lz⟩ : ∃ a : α, a ∈ Ioo y x ∧ l < f a := by
      simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_lt_csSup (h_nonempty.image _) hl
    filter_upwards [Ioo_mem_nhdsLT zx] with w hw
    exact lz.trans_le <| Mf ⟨yz, zx⟩ ⟨yz.trans_le hw.1.le, hw.2⟩ hw.1.le
  · rcases h_nonempty with ⟨_, hy, hx⟩
    filter_upwards [Ioo_mem_nhdsLT (hy.trans hx)] with w hw
    exact (le_csSup h_bdd (mem_image_of_mem _ hw)).trans_lt hm

Limit of Monotone Function at Left Endpoint of Open Interval Equals Supremum

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets with order topologies, where $\beta$ is conditionally complete. Let $f : \alpha \to \beta$ be a function that is monotone on the open interval $(y, x) \subseteq \alpha$, and suppose this interval is nonempty. If the image $f((y, x))$ is bounded above in $\beta$, then the limit of $f$ as the argument approaches $x$ from the left within $(y, x)$ exists and equals the supremum of $f((y, x))$ in $\beta$. In symbols: \[ \lim_{t \to x^-} f(t) = \sup_{t \in (y, x)} f(t) \]

MonotoneOn.tendsto_nhdsWithin_Ioo_right theorem

 {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β]
  [TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α} (h_nonempty : (Ioo x y).Nonempty)
  (Mf : MonotoneOn f (Ioo x y)) (h_bdd : BddBelow (f '' Ioo x y)) : Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioo x y)))

Full source

lemma MonotoneOn.tendsto_nhdsWithin_Ioo_right {α β : Type*} [LinearOrder α] [TopologicalSpace α]
    [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β]
    {f : α → β} {x y : α} (h_nonempty : (Ioo x y).Nonempty) (Mf : MonotoneOn f (Ioo x y))
    (h_bdd : BddBelow (f '' Ioo x y)) :
    Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioo x y))) := by
  refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩
  · rcases h_nonempty with ⟨p, hy, hx⟩
    filter_upwards [Ioo_mem_nhdsGT (hy.trans hx)] with w hw
    exact hl.trans_le <| csInf_le h_bdd (mem_image_of_mem _ hw)
  · obtain ⟨z, ⟨xz, zy⟩, zm⟩ : ∃ a : α, a ∈ Ioo x y ∧ f a < m := by
      simpa [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_csInf_lt (h_nonempty.image _) hm
    filter_upwards [Ioo_mem_nhdsGT xz] with w hw
    exact (Mf ⟨hw.1, hw.2.trans zy⟩ ⟨xz, zy⟩ hw.2.le).trans_lt zm

Limit of Monotone Function at Right Endpoint of Open Interval Equals Infimum

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets with order topologies, where $\beta$ is conditionally complete. Let $f : \alpha \to \beta$ be a function that is monotone on the open interval $(x, y) \subseteq \alpha$, and suppose this interval is nonempty. If the image $f((x, y))$ is bounded below in $\beta$, then the limit of $f$ as the argument approaches $x$ from the right within $(x, y)$ exists and equals the infimum of $f((x, y))$ in $\beta$. In symbols: \[ \lim_{t \to x^+} f(t) = \inf_{t \in (x, y)} f(t) \]

MonotoneOn.tendsto_nhdsLT theorem

 {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β]
  [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α} (Mf : MonotoneOn f (Iio x))
  (h_bdd : BddAbove (f '' Iio x)) : Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))

Full source

lemma MonotoneOn.tendsto_nhdsLT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
    [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α}
    (Mf : MonotoneOn f (Iio x)) (h_bdd : BddAbove (f '' Iio x)) :
    Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x))) := by
  rcases eq_empty_or_nonempty (Iio x) with (h | h); · simp [h]
  refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩
  · obtain ⟨z, zx, lz⟩ : ∃ a : α, a < x ∧ l < f a := by
      simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_lt_csSup (h.image _) hl
    filter_upwards [Ioo_mem_nhdsLT zx] with y hy using lz.trans_le (Mf zx hy.2 hy.1.le)
  · refine mem_of_superset self_mem_nhdsWithin fun y hy => lt_of_le_of_lt ?_ hm
    exact le_csSup h_bdd (mem_image_of_mem _ hy)

Limit of Monotone Function from Left Equals Supremum on Left Interval

Informal description

Let $\alpha$ and $\beta$ be types equipped with linear orders and order topologies, where $\beta$ is a conditionally complete linear order. Let $f : \alpha \to \beta$ be a function that is monotone on the interval $(-\infty, x) = \{y \mid y < x\}$. If the image $f((-\infty, x))$ is bounded above, then the limit of $f$ as $y$ approaches $x$ from the left exists and equals the supremum of $f((-\infty, x))$.

MonotoneOn.tendsto_nhdsGT theorem

 {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β]
  [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α} (Mf : MonotoneOn f (Ioi x))
  (h_bdd : BddBelow (f '' Ioi x)) : Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioi x)))

Full source

lemma MonotoneOn.tendsto_nhdsGT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
    [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α}
    (Mf : MonotoneOn f (Ioi x)) (h_bdd : BddBelow (f '' Ioi x)) :
    Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioi x))) :=
  MonotoneOn.tendsto_nhdsLT (α := αᵒᵈ) (β := βᵒᵈ) Mf.dual h_bdd

Limit of Monotone Function from Right Equals Infimum on Right Interval

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets equipped with order topologies, where $\beta$ is a conditionally complete linear order. Let $f : \alpha \to \beta$ be a function that is monotone on the right-infinite interval $(x, \infty) = \{y \mid y > x\}$. If the image $f((x, \infty))$ is bounded below, then the limit of $f$ as $y$ approaches $x$ from the right exists and equals the infimum of $f((x, \infty))$.

Monotone.tendsto_nhdsLT theorem

 {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β]
  [TopologicalSpace β] [OrderTopology β] {f : α → β} (Mf : Monotone f) (x : α) :
  Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))

Full source

/-- A monotone map has a limit to the left of any point `x`, equal to `sSup (f '' (Iio x))`. -/
theorem Monotone.tendsto_nhdsLT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
    [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β}
    (Mf : Monotone f) (x : α) : Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x))) :=
  MonotoneOn.tendsto_nhdsLT (Mf.monotoneOn _) (Mf.map_bddAbove bddAbove_Iio)

Left Limit of Monotone Function Equals Supremum on Left Interval

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets equipped with the order topology, where $\beta$ is a conditionally complete linear order. If $f : \alpha \to \beta$ is a monotone function, then for any $x \in \alpha$, the left limit of $f$ at $x$ exists and equals the supremum of the image of $f$ on the interval $(-\infty, x)$, i.e., \[ \lim_{y \to x^-} f(y) = \sup \{f(y) \mid y < x\}. \]

Monotone.tendsto_nhdsGT theorem

 {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β]
  [TopologicalSpace β] [OrderTopology β] {f : α → β} (Mf : Monotone f) (x : α) :
  Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioi x)))

Full source

/-- A monotone map has a limit to the right of any point `x`, equal to `sInf (f '' (Ioi x))`. -/
theorem Monotone.tendsto_nhdsGT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
    [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β}
    (Mf : Monotone f) (x : α) : Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioi x))) :=
  Monotone.tendsto_nhdsLT (α := αᵒᵈ) (β := βᵒᵈ) Mf.dual x

Right Limit of Monotone Function Equals Infimum on Right Interval

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets equipped with the order topology, where $\beta$ is a conditionally complete linear order. If $f : \alpha \to \beta$ is a monotone function, then for any $x \in \alpha$, the right limit of $f$ at $x$ exists and equals the infimum of the image of $f$ on the interval $(x, \infty)$, i.e., \[ \lim_{y \to x^+} f(y) = \inf \{f(y) \mid y > x\}. \]

AntitoneOn.tendsto_nhdsWithin_Ioo_left theorem

 {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β]
  [TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α} (h_nonempty : (Ioo y x).Nonempty)
  (Af : AntitoneOn f (Ioo y x)) (h_bdd : BddBelow (f '' Ioo y x)) : Tendsto f (𝓝[<] x) (𝓝 (sInf (f '' Ioo y x)))

Full source

lemma AntitoneOn.tendsto_nhdsWithin_Ioo_left {α β : Type*} [LinearOrder α] [TopologicalSpace α]
    [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β]
    {f : α → β} {x y : α} (h_nonempty : (Ioo y x).Nonempty) (Af : AntitoneOn f (Ioo y x))
    (h_bdd : BddBelow (f '' Ioo y x)) :
    Tendsto f (𝓝[<] x) (𝓝 (sInf (f '' Ioo y x))) :=
  MonotoneOn.tendsto_nhdsWithin_Ioo_left h_nonempty Af.dual_right h_bdd

Limit of Antitone Function at Left Endpoint of Open Interval Equals Infimum

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets with order topologies, where $\beta$ is conditionally complete. Let $f : \alpha \to \beta$ be a function that is antitone on the open interval $(y, x) \subseteq \alpha$, and suppose this interval is nonempty. If the image $f((y, x))$ is bounded below in $\beta$, then the limit of $f$ as the argument approaches $x$ from the left within $(y, x)$ exists and equals the infimum of $f((y, x))$ in $\beta$. In symbols: \[ \lim_{t \to x^-} f(t) = \inf_{t \in (y, x)} f(t) \]

AntitoneOn.tendsto_nhdsWithin_Ioo_right theorem

 {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β]
  [TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α} (h_nonempty : (Ioo x y).Nonempty)
  (Af : AntitoneOn f (Ioo x y)) (h_bdd : BddAbove (f '' Ioo x y)) : Tendsto f (𝓝[>] x) (𝓝 (sSup (f '' Ioo x y)))

Full source

lemma AntitoneOn.tendsto_nhdsWithin_Ioo_right {α β : Type*} [LinearOrder α] [TopologicalSpace α]
    [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β]
    {f : α → β} {x y : α} (h_nonempty : (Ioo x y).Nonempty) (Af : AntitoneOn f (Ioo x y))
    (h_bdd : BddAbove (f '' Ioo x y)) :
    Tendsto f (𝓝[>] x) (𝓝 (sSup (f '' Ioo x y))) :=
  MonotoneOn.tendsto_nhdsWithin_Ioo_right h_nonempty Af.dual_right h_bdd

Limit of Antitone Function at Right Endpoint of Open Interval Equals Supremum

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets equipped with order topologies, where $\beta$ is a conditionally complete linear order. Let $f : \alpha \to \beta$ be a function that is antitone on the open interval $(x, y) \subseteq \alpha$, and suppose this interval is nonempty. If the image $f((x, y))$ is bounded above in $\beta$, then the limit of $f$ as the argument approaches $x$ from the right within $(x, y)$ exists and equals the supremum of $f((x, y))$ in $\beta$. In symbols: \[ \lim_{t \to x^+} f(t) = \sup_{t \in (x, y)} f(t) \]

AntitoneOn.tendsto_nhdsLT theorem

 {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β]
  [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α} (Af : AntitoneOn f (Iio x))
  (h_bdd : BddBelow (f '' Iio x)) : Tendsto f (𝓝[<] x) (𝓝 (sInf (f '' Iio x)))

Full source

lemma AntitoneOn.tendsto_nhdsLT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
    [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α}
    (Af : AntitoneOn f (Iio x)) (h_bdd : BddBelow (f '' Iio x)) :
    Tendsto f (𝓝[<] x) (𝓝 (sInf (f '' Iio x))) :=
  MonotoneOn.tendsto_nhdsLT Af.dual_right h_bdd

Limit of Antitone Function from Left Equals Infimum on Left Interval

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets equipped with order topologies, where $\beta$ is a conditionally complete linear order. Let $f : \alpha \to \beta$ be a function that is antitone on the interval $(-\infty, x) = \{y \mid y < x\}$. If the image $f((-\infty, x))$ is bounded below, then the limit of $f$ as $y$ approaches $x$ from the left exists and equals the infimum of $f((-\infty, x))$.

AntitoneOn.tendsto_nhdsGT theorem

 {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β]
  [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α} (Af : AntitoneOn f (Ioi x))
  (h_bdd : BddAbove (f '' Ioi x)) : Tendsto f (𝓝[>] x) (𝓝 (sSup (f '' Ioi x)))

Full source

lemma AntitoneOn.tendsto_nhdsGT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
    [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α}
    (Af : AntitoneOn f (Ioi x)) (h_bdd : BddAbove (f '' Ioi x)) :
    Tendsto f (𝓝[>] x) (𝓝 (sSup (f '' Ioi x))) :=
  MonotoneOn.tendsto_nhdsGT Af.dual_right h_bdd

Limit of Antitone Function from Right Equals Supremum on Right Interval

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets equipped with order topologies, where $\beta$ is a conditionally complete linear order. Let $f : \alpha \to \beta$ be a function that is antitone on the right-infinite interval $(x, \infty)$. If the image $f((x, \infty))$ is bounded above, then the limit of $f$ as $y$ approaches $x$ from the right exists and equals the supremum of $f((x, \infty))$.

Antitone.tendsto_nhdsLT theorem

 {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β]
  [TopologicalSpace β] [OrderTopology β] {f : α → β} (Af : Antitone f) (x : α) :
  Tendsto f (𝓝[<] x) (𝓝 (sInf (f '' Iio x)))

Full source

/-- An antitone map has a limit to the left of any point `x`, equal to `sInf (f '' (Iio x))`. -/
theorem Antitone.tendsto_nhdsLT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
    [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β}
    (Af : Antitone f) (x : α) : Tendsto f (𝓝[<] x) (𝓝 (sInf (f '' Iio x))) :=
  Monotone.tendsto_nhdsLT Af.dual_right x

Left Limit of Antitone Function Equals Infimum on Left Interval

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets equipped with the order topology, where $\beta$ is a conditionally complete linear order. If $f : \alpha \to \beta$ is an antitone function, then for any $x \in \alpha$, the left limit of $f$ at $x$ exists and equals the infimum of the image of $f$ on the interval $(-\infty, x)$, i.e., \[ \lim_{y \to x^-} f(y) = \inf \{f(y) \mid y < x\}. \]

Antitone.tendsto_nhdsGT theorem

 {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β]
  [TopologicalSpace β] [OrderTopology β] {f : α → β} (Af : Antitone f) (x : α) :
  Tendsto f (𝓝[>] x) (𝓝 (sSup (f '' Ioi x)))

Full source

/-- An antitone map has a limit to the right of any point `x`, equal to `sSup (f '' (Ioi x))`. -/
theorem Antitone.tendsto_nhdsGT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
    [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β}
    (Af : Antitone f) (x : α) : Tendsto f (𝓝[>] x) (𝓝 (sSup (f '' Ioi x))) :=
  Monotone.tendsto_nhdsGT Af.dual_right x

Right Limit of Antitone Function Equals Supremum on Right Interval

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets equipped with the order topology, where $\beta$ is a conditionally complete linear order. If $f : \alpha \to \beta$ is an antitone function, then for any $x \in \alpha$, the right limit of $f$ at $x$ exists and equals the supremum of the image of $f$ on the interval $(x, \infty)$, i.e., \[ \lim_{y \to x^+} f(y) = \sup \{f(y) \mid y > x\}. \]