# Monotone functions on an order topology #

This file contains lemmas about limits and continuity for monotone / antitone functions on linearly-ordered sets (with the order topology). For example, we prove that a monotone function has left and right limits at any point (Monotone.tendsto_nhdsWithin_Iio, Monotone.tendsto_nhdsWithin_Ioi).

theorem Monotone.map_sSup_of_continuousAt' {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {A : Set α} (Cf : ContinuousAt f (sSup A)) (Mf : ) (A_nonemp : A.Nonempty) (A_bdd : ) :
f (sSup A) = sSup (f '' A)

A monotone function continuous at the supremum of a nonempty set sends this supremum to the supremum of the image of this set.

theorem Monotone.map_iSup_of_continuousAt' {α : Type u_1} {β : Type u_2} [] [] [] {ι : Sort u_4} [] {f : αβ} {g : ια} (Cf : ContinuousAt f (iSup g)) (Mf : ) (bdd : ) :
f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

A monotone function continuous at the indexed supremum over a nonempty Sort sends this indexed supremum to the indexed supremum of the composition.

theorem Monotone.map_sInf_of_continuousAt' {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {A : Set α} (Cf : ContinuousAt f (sInf A)) (Mf : ) (A_nonemp : A.Nonempty) (A_bdd : ) :
f (sInf A) = sInf (f '' A)

A monotone function continuous at the infimum of a nonempty set sends this infimum to the infimum of the image of this set.

theorem Monotone.map_iInf_of_continuousAt' {α : Type u_1} {β : Type u_2} [] [] [] {ι : Sort u_4} [] {f : αβ} {g : ια} (Cf : ContinuousAt f (iInf g)) (Mf : ) (bdd : ) :
f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)

A monotone function continuous at the indexed infimum over a nonempty Sort sends this indexed infimum to the indexed infimum of the composition.

theorem Antitone.map_sInf_of_continuousAt' {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {A : Set α} (Cf : ContinuousAt f (sInf A)) (Af : ) (A_nonemp : A.Nonempty) (A_bdd : ) :
f (sInf A) = sSup (f '' A)

An antitone function continuous at the infimum of a nonempty set sends this infimum to the supremum of the image of this set.

theorem Antitone.map_iInf_of_continuousAt' {α : Type u_1} {β : Type u_2} [] [] [] {ι : Sort u_4} [] {f : αβ} {g : ια} (Cf : ContinuousAt f (iInf g)) (Af : ) (bdd : ) :
f (⨅ (i : ι), g i) = ⨆ (i : ι), f (g i)

An antitone function continuous at the indexed infimum over a nonempty Sort sends this indexed infimum to the indexed supremum of the composition.

theorem Antitone.map_sSup_of_continuousAt' {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {A : Set α} (Cf : ContinuousAt f (sSup A)) (Af : ) (A_nonemp : A.Nonempty) (A_bdd : ) :
f (sSup A) = sInf (f '' A)

An antitone function continuous at the supremum of a nonempty set sends this supremum to the infimum of the image of this set.

theorem Antitone.map_iSup_of_continuousAt' {α : Type u_1} {β : Type u_2} [] [] [] {ι : Sort u_4} [] {f : αβ} {g : ια} (Cf : ContinuousAt f (iSup g)) (Af : ) (bdd : ) :
f (⨆ (i : ι), g i) = ⨅ (i : ι), f (g i)

An antitone function continuous at the indexed supremum over a nonempty Sort sends this indexed supremum to the indexed infimum of the composition.

theorem sSup_mem_closure {α : Type u_1} [] [] {s : Set α} (hs : s.Nonempty) :
theorem sInf_mem_closure {α : Type u_1} [] [] {s : Set α} (hs : s.Nonempty) :
theorem IsClosed.sSup_mem {α : Type u_1} [] [] {s : Set α} (hs : s.Nonempty) (hc : ) :
sSup s s
theorem IsClosed.sInf_mem {α : Type u_1} [] [] {s : Set α} (hs : s.Nonempty) (hc : ) :
sInf s s
theorem Monotone.map_sSup_of_continuousAt {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Mf : ) (fbot : f = ) :
f (sSup s) = sSup (f '' s)

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_iSup_of_continuousAt {α : Type u_1} {β : Type u_2} [] [] [] {ι : Sort u_4} {f : αβ} {g : ια} (Cf : ContinuousAt f (iSup g)) (Mf : ) (fbot : f = ) :
f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

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_sInf_of_continuousAt {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Mf : ) (ftop : f = ) :
f (sInf s) = sInf (f '' s)

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_iInf_of_continuousAt {α : Type u_1} {β : Type u_2} [] [] [] {ι : Sort u_4} {f : αβ} {g : ια} (Cf : ContinuousAt f (iInf g)) (Mf : ) (ftop : f = ) :
f (iInf g) = iInf (f g)

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 Antitone.map_sSup_of_continuousAt {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Af : ) (fbot : f = ) :
f (sSup s) = sInf (f '' s)

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_iSup_of_continuousAt {α : Type u_1} {β : Type u_2} [] [] [] {ι : Sort u_4} {f : αβ} {g : ια} (Cf : ContinuousAt f (iSup g)) (Af : ) (fbot : f = ) :
f (⨆ (i : ι), g i) = ⨅ (i : ι), f (g i)

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_sInf_of_continuousAt {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Af : ) (ftop : f = ) :
f (sInf s) = sSup (f '' s)

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_iInf_of_continuousAt {α : Type u_1} {β : Type u_2} [] [] [] {ι : Sort u_4} {f : αβ} {g : ια} (Cf : ContinuousAt f (iInf g)) (Af : ) (ftop : f = ) :
f (iInf g) = iSup (f g)

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 csSup_mem_closure {α : Type u_1} [] [] {s : Set α} (hs : s.Nonempty) (B : ) :
theorem csInf_mem_closure {α : Type u_1} [] [] {s : Set α} (hs : s.Nonempty) (B : ) :
theorem IsClosed.csSup_mem {α : Type u_1} [] [] {s : Set α} (hc : ) (hs : s.Nonempty) (B : ) :
sSup s s
theorem IsClosed.csInf_mem {α : Type u_1} [] [] {s : Set α} (hc : ) (hs : s.Nonempty) (B : ) :
sInf s s
theorem IsClosed.isLeast_csInf {α : Type u_1} [] [] {s : Set α} (hc : ) (hs : s.Nonempty) (B : ) :
theorem IsClosed.isGreatest_csSup {α : Type u_1} [] [] {s : Set α} (hc : ) (hs : s.Nonempty) (B : ) :
theorem Monotone.map_csSup_of_continuousAt {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Mf : ) (ne : s.Nonempty) (H : ) :
f (sSup s) = sSup (f '' s)

If a monotone function is continuous at the supremum of a nonempty bounded above set s, then it sends this supremum to the supremum of the image of s.

theorem Monotone.map_ciSup_of_continuousAt {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : αβ} {g : γα} (Cf : ContinuousAt f (⨆ (i : γ), g i)) (Mf : ) (H : ) :
f (⨆ (i : γ), g i) = ⨆ (i : γ), f (g i)

If a monotone function is continuous at the indexed supremum of a bounded function on a nonempty Sort, then it sends this supremum to the supremum of the composition.

theorem Monotone.map_csInf_of_continuousAt {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Mf : ) (ne : s.Nonempty) (H : ) :
f (sInf s) = sInf (f '' s)

If a monotone function is continuous at the infimum of a nonempty bounded below set s, then it sends this infimum to the infimum of the image of s.

theorem Monotone.map_ciInf_of_continuousAt {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : αβ} {g : γα} (Cf : ContinuousAt f (⨅ (i : γ), g i)) (Mf : ) (H : ) :
f (⨅ (i : γ), g i) = ⨅ (i : γ), f (g i)

A continuous monotone function sends indexed infimum to indexed infimum in conditionally complete linear order, under a boundedness assumption.

theorem Antitone.map_csSup_of_continuousAt {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Af : ) (ne : s.Nonempty) (H : ) :
f (sSup s) = sInf (f '' s)

If an antitone function is continuous at the supremum of a nonempty bounded above set s, then it sends this supremum to the infimum of the image of s.

theorem Antitone.map_ciSup_of_continuousAt {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : αβ} {g : γα} (Cf : ContinuousAt f (⨆ (i : γ), g i)) (Af : ) (H : ) :
f (⨆ (i : γ), g i) = ⨅ (i : γ), f (g i)

If an antitone function is continuous at the indexed supremum of a bounded function on a nonempty Sort, then it sends this supremum to the infimum of the composition.

theorem Antitone.map_csInf_of_continuousAt {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Af : ) (ne : s.Nonempty) (H : ) :
f (sInf s) = sSup (f '' s)

If an antitone function is continuous at the infimum of a nonempty bounded below set s, then it sends this infimum to the supremum of the image of s.

theorem Antitone.map_ciInf_of_continuousAt {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : αβ} {g : γα} (Cf : ContinuousAt f (⨅ (i : γ), g i)) (Af : ) (H : ) :
f (⨅ (i : γ), g i) = ⨆ (i : γ), f (g i)

A continuous antitone function sends indexed infimum to indexed supremum in conditionally complete linear order, under a boundedness assumption.

theorem Monotone.tendsto_nhdsWithin_Iio {α : Type u_4} {β : Type u_5} [] [] [] [] [] {f : αβ} (Mf : ) (x : α) :

A monotone map has a limit to the left of any point x, equal to sSup (f '' (Iio x)).

theorem Monotone.tendsto_nhdsWithin_Ioi {α : Type u_4} {β : Type u_5} [] [] [] [] [] {f : αβ} (Mf : ) (x : α) :

A monotone map has a limit to the right of any point x, equal to sInf (f '' (Ioi x)).