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_nhdsLT, Monotone.tendsto_nhdsGT).

theorem MonotoneOn.insert_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {x : α} {f : α → β} [TopologicalSpace β] [OrderClosedTopology β] (hf : MonotoneOn f s) (hx : ClusterPt x (Filter.principal s)) (h'x : ContinuousWithinAt f s x) : MonotoneOn f (insert x s)

theorem MonotoneOn.countable_setOf_two_preimages {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {f : α → β} [SecondCountableTopology α] (hf : MonotoneOn f s) : {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable

If a function is monotone on a set in a second countable topological space, then there are only countably many points that have several preimages.

theorem Monotone.countable_setOf_two_preimages {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {f : α → β} [SecondCountableTopology α] (hf : Monotone f) : {c : β | ∃ (x : α) (y : α), x < y ∧ f x = c ∧ f y = c}.Countable

If a function is monotone in a second countable topological space, then there are only countably many points that have several preimages.

theorem AntitoneOn.countable_setOf_two_preimages {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {f : α → β} [SecondCountableTopology α] (hf : AntitoneOn f s) : {c : β | ∃ (x : α) (y : α), x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable

If a function is antitone on a set in a second countable topological space, then there are only countably many points that have several preimages.

theorem Antitone.countable_setOf_two_preimages {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {f : α → β} [SecondCountableTopology α] (hf : Antitone f) : {c : β | ∃ (x : α) (y : α), x < y ∧ f x = c ∧ f y = c}.Countable

If a function is antitone in a second countable topological space, then there are only countably many points that have several preimages.

theorem MonotoneOn.countable_not_continuousWithinAt_Ioi {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {f : α → β} [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] (hf : MonotoneOn f s) : {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Set.Ioi x) x}.Countable

In a second countable space, the set of points where a monotone function is not right-continuous within a set is at most countable. Superseded by MonotoneOn.countable_not_continuousWithinAt which gives the two-sided version.

theorem MonotoneOn.countable_not_continuousWithinAt_Iio {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {f : α → β} [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] (hf : MonotoneOn f s) : {x : α | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Set.Iio x) x}.Countable

In a second countable space, the set of points where a monotone function is not left-continuous within a set is at most countable. Superseded by MonotoneOn.countable_not_continuousWithinAt which gives the two-sided version.

theorem MonotoneOn.countable_not_continuousWithinAt {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {f : α → β} [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] (hf : MonotoneOn f s) : {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}.Countable

In a second countable space, the set of points where a monotone function is not continuous within a set is at most countable.

theorem Monotone.countable_not_continuousAt {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {f : α → β} [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] (hf : Monotone f) : {x : α | ¬ContinuousAt f x}.Countable

In a second countable space, the set of points where a monotone function is not continuous is at most countable.

theorem AntitoneOn.countable_not_continuousWithinAt {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {f : α → β} [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] {s : Set α} (hf : AntitoneOn f s) : {x : α | x ∈ s ∧ ¬ContinuousWithinAt f s x}.Countable

In a second countable space, the set of points where an antitone function is not continuous within a set is at most countable.

theorem Antitone.countable_not_continuousAt {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {f : α → β} [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] (hf : Antitone f) : {x : α | ¬ContinuousAt f x}.Countable

In a second countable space, the set of points where an antitone function is not continuous is at most countable.

theorem MonotoneOn.map_csSup_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousWithinAt f A (sSup A)) (Mf : MonotoneOn f A) (A_nonemp : A.Nonempty) (A_bdd : BddAbove A := by bddDefault) : 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_csSup_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 : BddAbove A := by bddDefault) : 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_ciSup_of_continuousAt {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Mf : Monotone f) (bdd : BddAbove (Set.range g) := by bddDefault) : 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 MonotoneOn.map_csInf_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousWithinAt f A (sInf A)) (Mf : MonotoneOn f A) (A_nonemp : A.Nonempty) (A_bdd : BddBelow A := by bddDefault) : 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_csInf_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 : BddBelow A := by bddDefault) : 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_ciInf_of_continuousAt {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Mf : Monotone f) (bdd : BddBelow (Set.range g) := by bddDefault) : 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 AntitoneOn.map_csInf_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousWithinAt f A (sInf A)) (Af : AntitoneOn f A) (A_nonemp : A.Nonempty) (A_bdd : BddBelow A := by bddDefault) : 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_csInf_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 : BddBelow A := by bddDefault) : 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_ciInf_of_continuousAt {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Af : Antitone f) (bdd : BddBelow (Set.range g) := by bddDefault) : 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 AntitoneOn.map_csSup_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousWithinAt f A (sSup A)) (Af : AntitoneOn f A) (A_nonemp : A.Nonempty) (A_bdd : BddAbove A := by bddDefault) : 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_csSup_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 : BddAbove A := by bddDefault) : 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_ciSup_of_continuousAt {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Af : Antitone f) (bdd : BddAbove (Set.range g) := by bddDefault) : 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 MonotoneOn.map_sSup_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sSup s)) (Mf : MonotoneOn f s) (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_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_3} {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 MonotoneOn.map_sInf_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sInf s)) (Mf : MonotoneOn f s) (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_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_3} {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 AntitoneOn.map_sSup_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sSup s)) (Af : AntitoneOn f s) (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_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_3} {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 AntitoneOn.map_sInf_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sInf s)) (Af : AntitoneOn f s) (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_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_3} {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 MonotoneOn.tendsto_nhdsWithin_Ioo_left {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α} (h_nonempty : (Set.Ioo y x).Nonempty) (Mf : MonotoneOn f (Set.Ioo y x)) (h_bdd : BddAbove (f '' Set.Ioo y x)) : Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sSup (f '' Set.Ioo y x)))

theorem MonotoneOn.tendsto_nhdsWithin_Ioo_right {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α} (h_nonempty : (Set.Ioo x y).Nonempty) (Mf : MonotoneOn f (Set.Ioo x y)) (h_bdd : BddBelow (f '' Set.Ioo x y)) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sInf (f '' Set.Ioo x y)))

theorem MonotoneOn.tendsto_nhdsLT {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α} (Mf : MonotoneOn f (Set.Iio x)) (h_bdd : BddAbove (f '' Set.Iio x)) : Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sSup (f '' Set.Iio x)))

theorem MonotoneOn.tendsto_nhdsGT {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α} (Mf : MonotoneOn f (Set.Ioi x)) (h_bdd : BddBelow (f '' Set.Ioi x)) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sInf (f '' Set.Ioi x)))

theorem Monotone.tendsto_nhdsLT {α : Type u_3} {β : Type u_4} [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_nhdsGT {α : Type u_3} {β : Type u_4} [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)).

theorem AntitoneOn.tendsto_nhdsWithin_Ioo_left {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α} (h_nonempty : (Set.Ioo y x).Nonempty) (Af : AntitoneOn f (Set.Ioo y x)) (h_bdd : BddBelow (f '' Set.Ioo y x)) : Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sInf (f '' Set.Ioo y x)))

theorem AntitoneOn.tendsto_nhdsWithin_Ioo_right {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α} (h_nonempty : (Set.Ioo x y).Nonempty) (Af : AntitoneOn f (Set.Ioo x y)) (h_bdd : BddAbove (f '' Set.Ioo x y)) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sSup (f '' Set.Ioo x y)))

theorem AntitoneOn.tendsto_nhdsLT {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α} (Af : AntitoneOn f (Set.Iio x)) (h_bdd : BddBelow (f '' Set.Iio x)) : Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sInf (f '' Set.Iio x)))

theorem AntitoneOn.tendsto_nhdsGT {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α} (Af : AntitoneOn f (Set.Ioi x)) (h_bdd : BddAbove (f '' Set.Ioi x)) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sSup (f '' Set.Ioi x)))

theorem Antitone.tendsto_nhdsLT {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (Af : Antitone f) (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sInf (f '' Set.Iio x)))

An antitone map has a limit to the left of any point x, equal to sInf (f '' (Iio x)).

theorem Antitone.tendsto_nhdsGT {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (Af : Antitone f) (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sSup (f '' Set.Ioi x)))

An antitone map has a limit to the right of any point x, equal to sSup (f '' (Ioi x)).