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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousAt f (sSup A)) (Mf : Monotone f) (A_nonemp : A.Nonempty) (A_bdd : autoParam (BddAbove A) _auto✝) : 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_4} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Mf : Monotone f) (bdd : autoParam (BddAbove (Set.range g)) _auto✝) : 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousAt f (sInf A)) (Mf : Monotone f) (A_nonemp : A.Nonempty) (A_bdd : autoParam (BddBelow A) _auto✝) : 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_4} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Mf : Monotone f) (bdd : autoParam (BddBelow (Set.range g)) _auto✝) : 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousAt f (sInf A)) (Af : Antitone f) (A_nonemp : A.Nonempty) (A_bdd : autoParam (BddBelow A) _auto✝) : 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_4} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Af : Antitone f) (bdd : autoParam (BddBelow (Set.range g)) _auto✝) : 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousAt f (sSup A)) (Af : Antitone f) (A_nonemp : A.Nonempty) (A_bdd : autoParam (BddAbove A) _auto✝) : 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_4} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Af : Antitone f) (bdd : autoParam (BddAbove (Set.range g)) _auto✝) : 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} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hs : s.Nonempty) : sSup s ∈ closure s

theorem sInf_mem_closure {α : Type u_1} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hs : s.Nonempty) : sInf s ∈ closure s

theorem IsClosed.sSup_mem {α : Type u_1} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hs : s.Nonempty) (hc : IsClosed s) : sSup s ∈ s

theorem IsClosed.sInf_mem {α : Type u_1} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hs : s.Nonempty) (hc : IsClosed s) : sInf s ∈ s

theorem Monotone.map_sSup_of_continuousAt {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Mf : Monotone f) (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} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_4} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Mf : Monotone f) (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} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Mf : Monotone f) (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} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_4} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Mf : Monotone f) (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} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Af : Antitone f) (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} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_4} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Af : Antitone f) (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} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Af : Antitone f) (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} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_4} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Af : Antitone f) (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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hs : s.Nonempty) (B : BddAbove s) : sSup s ∈ closure s

theorem csInf_mem_closure {α : Type u_1} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hs : s.Nonempty) (B : BddBelow s) : sInf s ∈ closure s

theorem IsClosed.csSup_mem {α : Type u_1} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddAbove s) : sSup s ∈ s

theorem IsClosed.csInf_mem {α : Type u_1} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddBelow s) : sInf s ∈ s

theorem IsClosed.isLeast_csInf {α : Type u_1} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddBelow s) : IsLeast s (sInf s)

theorem IsClosed.isGreatest_csSup {α : Type u_1} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddAbove s) : IsGreatest s (sSup s)

theorem Monotone.map_csSup_of_continuousAt {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Mf : Monotone f) (ne : s.Nonempty) (H : BddAbove s) : 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] [Nonempty γ] {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨆ (i : γ), g i)) (Mf : Monotone f) (H : BddAbove (Set.range g)) : 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Mf : Monotone f) (ne : s.Nonempty) (H : BddBelow s) : 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] [Nonempty γ] {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨅ (i : γ), g i)) (Mf : Monotone f) (H : BddBelow (Set.range g)) : 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Af : Antitone f) (ne : s.Nonempty) (H : BddAbove s) : 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] [Nonempty γ] {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨆ (i : γ), g i)) (Af : Antitone f) (H : BddAbove (Set.range g)) : 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Af : Antitone f) (ne : s.Nonempty) (H : BddBelow s) : 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] [Nonempty γ] {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨅ (i : γ), g i)) (Af : Antitone f) (H : BddBelow (Set.range g)) : 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} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (Mf : Monotone f) (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sSup (f '' Set.Iio 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} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (Mf : Monotone f) (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sInf (f '' Set.Ioi x)))

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