Left and right limits within a set

theorem nhdsWithin_inf_principal {E : Type u_1} [TopologicalSpace E] (s t : Set E) (x : E) : nhdsWithin x s ⊓ Filter.principal t = nhdsWithin x (s ∩ t)

noncomputable def Function.leftLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] (f : α → β) (s : Set α) (a : α) : β

Let f : α → β be a function from a linear order α to a topological space β, and let a : α. The limit strictly to the left of f at a, denoted with leftLim f a, is defined by using the order topology on α. If a is isolated to its left or the function has no left limit, we use f a instead to guarantee a good behavior in most cases.

Equations

• Function.leftLimWithin f s a = if nhdsWithin a (Set.Iio a ∩ s) = ⊥ ∨ ¬∃ (y : β), Filter.Tendsto f (nhdsWithin a (Set.Iio a ∩ s)) (nhds y) then f a else (nhdsWithin a (Set.Iio a ∩ s)).limUnder f

noncomputable def Function.rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] (f : α → β) (s : Set α) (a : α) : β

Let f : α → β be a function from a linear order α to a topological space β, and let a : α. The limit strictly to the right of f at a, denoted with rightLim f a, is defined by using the order topology on α. If a is isolated to its right or the function has no right limit, we use f a instead to guarantee a good behavior in most cases.

Equations

• Function.rightLimWithin f s a = Function.leftLimWithin f s a

The within-neighbourhood filter is NeBot under a density hypothesis

theorem nhdsWithin_Iio_inter_neBot_of_nhdsLT_neBot {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hs : Dense s) (a : α) [(nhdsWithin a (Set.Iio a)).NeBot] : (nhdsWithin a (Set.Iio a ∩ s)).NeBot

If s is dense and 𝓝[<] a is not bot, then a is a left-accumulation point of s.

theorem nhdsWithin_Iio_inter_neBot {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {s : Set α} (hs : Dense s) (a : α) : (nhdsWithin a (Set.Iio a ∩ s)).NeBot

If s is dense and a is not a minimum, then a is a left-accumulation point of s.

theorem nhdsWithin_Ioi_inter_neBot_of_nhdsGT_neBot {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hs : Dense s) (a : α) [(nhdsWithin a (Set.Ioi a)).NeBot] : (nhdsWithin a (Set.Ioi a ∩ s)).NeBot

If s is dense and 𝓝[>] a is not bot, then a is a right-accumulation point of s.

theorem nhdsWithin_Ioi_inter_neBot {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {s : Set α} (hs : Dense s) (a : α) : (nhdsWithin a (Set.Ioi a ∩ s)).NeBot

If s is dense and a is not a maximum, then a is a right-accumulation point of s.

Basic characterisations of the within left/right limit

theorem leftLimWithin_eq_of_tendsto {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [hα : TopologicalSpace α] [h'α : OrderTopology α] [T2Space β] {f : α → β} {s : Set α} {a : α} {y : β} [h : (nhdsWithin a (Set.Iio a ∩ s)).NeBot] (h' : Filter.Tendsto f (nhdsWithin a (Set.Iio a ∩ s)) (nhds y)) : Function.leftLimWithin f s a = y

theorem rightLimWithin_eq_of_tendsto {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [T2Space β] {f : α → β} {s : Set α} {a : α} {y : β} [h : (nhdsWithin a (Set.Ioi a ∩ s)).NeBot] (h' : Filter.Tendsto f (nhdsWithin a (Set.Ioi a ∩ s)) (nhds y)) : Function.rightLimWithin f s a = y

theorem leftLimWithin_eq_of_eq_bot {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [hα : TopologicalSpace α] [h'α : OrderTopology α] (f : α → β) {s : Set α} {a : α} (h : nhdsWithin a (Set.Iio a ∩ s) = ⊥) : Function.leftLimWithin f s a = f a

theorem rightLimWithin_eq_of_eq_bot {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] (f : α → β) {s : Set α} {a : α} (h : nhdsWithin a (Set.Ioi a ∩ s) = ⊥) : Function.rightLimWithin f s a = f a

theorem leftLimWithin_eq_of_nhdsLT_eq_bot {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] (f : α → β) (s : Set α) {a : α} (h : nhdsWithin a (Set.Iio a) = ⊥) : Function.leftLimWithin f s a = f a

At a point which is isolated on the left, the within left limit is the value of the function.

theorem rightLimWithin_eq_of_nhdsGT_eq_bot {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] (f : α → β) (s : Set α) {a : α} (h : nhdsWithin a (Set.Ioi a) = ⊥) : Function.rightLimWithin f s a = f a

At a point which is isolated on the right, the within right limit is the value of the function.

theorem leftLimWithin_eq_of_not_tendsto {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [hα : TopologicalSpace α] [h'α : OrderTopology α] (f : α → β) {s : Set α} {a : α} (h : ¬∃ (y : β), Filter.Tendsto f (nhdsWithin a (Set.Iio a ∩ s)) (nhds y)) : Function.leftLimWithin f s a = f a

theorem rightLimWithin_eq_of_not_tendsto {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [hα : TopologicalSpace α] [h'α : OrderTopology α] (f : α → β) {s : Set α} {a : α} (h : ¬∃ (y : β), Filter.Tendsto f (nhdsWithin a (Set.Ioi a ∩ s)) (nhds y)) : Function.rightLimWithin f s a = f a

theorem leftLimWithin_eq_of_isBot {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] {f : α → β} {s : Set α} {a : α} (ha : IsBot a) : Function.leftLimWithin f s a = f a

theorem rightLimWithin_eq_of_isTop {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] {f : α → β} {s : Set α} {a : α} (ha : IsTop a) : Function.rightLimWithin f s a = f a

theorem ContinuousWithinAt.leftLimWithin_eq {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [T2Space β] {f : α → β} {s : Set α} {a : α} (hf : ContinuousWithinAt f (Set.Iic a ∩ s) a) : Function.leftLimWithin f s a = f a

theorem ContinuousWithinAt.rightLimWithin_eq {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [T2Space β] {f : α → β} {s : Set α} {a : α} (hf : ContinuousWithinAt f (Set.Ici a ∩ s) a) : Function.rightLimWithin f s a = f a

theorem tendsto_leftLimWithin_of_tendsto {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [h'α : OrderTopology α] {f : α → β} {s : Set α} {a : α} (h : ∃ (y : β), Filter.Tendsto f (nhdsWithin a (Set.Iio a ∩ s)) (nhds y)) : Filter.Tendsto f (nhdsWithin a (Set.Iio a ∩ s)) (nhds (Function.leftLimWithin f s a))

theorem tendsto_rightLimWithin_of_tendsto {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] {f : α → β} {s : Set α} {a : α} (h : ∃ (y : β), Filter.Tendsto f (nhdsWithin a (Set.Ioi a ∩ s)) (nhds y)) : Filter.Tendsto f (nhdsWithin a (Set.Ioi a ∩ s)) (nhds (Function.rightLimWithin f s a))

theorem mapClusterPt_leftLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] (f : α → β) {s : Set α} {a : α} (ha : a ∈ s) : MapClusterPt (Function.leftLimWithin f s a) (nhdsWithin a (Set.Iic a ∩ s)) f

The within left limit is a cluster point of f along the closed left within-neighbourhood, provided a ∈ s.

theorem mapClusterPt_rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] (f : α → β) {s : Set α} {a : α} (ha : a ∈ s) : MapClusterPt (Function.rightLimWithin f s a) (nhdsWithin a (Set.Ici a ∩ s)) f

Regularisation: the within left/right limit is one-sided continuous within s

These mirror the original continuousWithinAt_leftLim_Iic etc.: they take only the single-point hypothesis that f admits a within left (resp. right) limit at a, and split into cases according to whether the within-neighbourhood at each nearby point is ⊥, has no limit, or has a limit. The conclusions are stated within s (Iic a ∩ s in place of Iic a); restricting to s is what lets the degenerate cases go through, so no density hypothesis is needed.

theorem continuousWithinAt_leftLimWithin_Iic {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [T3Space β] {f : α → β} {s : Set α} {a : α} (h : Filter.Tendsto f (nhdsWithin a (Set.Iio a ∩ s)) (nhds (Function.leftLimWithin f s a))) : ContinuousWithinAt (Function.leftLimWithin f s) (Set.Iic a ∩ s) a

theorem continuousWithinAt_rightLimWithin_Ici {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [T3Space β] {f : α → β} {s : Set α} {a : α} (h : Filter.Tendsto f (nhdsWithin a (Set.Ioi a ∩ s)) (nhds (Function.rightLimWithin f s a))) : ContinuousWithinAt (Function.rightLimWithin f s) (Set.Ici a ∩ s) a

theorem nhdsWithin_Iio_inter_neBot_of_exists_lt {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) {a : α} (ha : ∃ (b : α), b < a) : (nhdsWithin a (Set.Iio a ∩ s)).NeBot

If s is dense and a is not a minimum, then a is a right-accumulation point of s. Version of nhdsWithin_Iio_inter_neBot for an order which may have a maximal element.

theorem nhdsWithin_Ioi_inter_neBot_of_exists_gt {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) {a : α} (ha : ∃ (b : α), a < b) : (nhdsWithin a (Set.Ioi a ∩ s)).NeBot

If s is dense and a is not a maximum, then a is a right-accumulation point of s. Version of nhdsWithin_Iio_inter_neBot for an order which may have a maximal element.

theorem continuousWithinAt_leftLimWithin_Iic_of_dense {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [T3Space β] {f : α → β} {s : Set α} {a : α} (hs : Dense s) (hs' : ∀ᶠ (c : α) in nhdsWithin a (Set.Iio a), nhdsWithin c (Set.Iio c) = ⊥ → c ∈ s) (h : Filter.Tendsto f (nhdsWithin a (Set.Iio a ∩ s)) (nhds (Function.leftLimWithin f s a))) (hlim : ∀ᶠ (c : α) in nhdsWithin a (Set.Iio a), Filter.Tendsto f (nhdsWithin c (Set.Iio c ∩ s)) (nhds (Function.leftLimWithin f s c))) : ContinuousWithinAt (Function.leftLimWithin f s) (Set.Iic a) a

Dense version of continuousWithinAt_leftLimWithin_Iic with the stronger conclusion that the regularisation is continuous along the full left neighbourhood Iic a. This needs s dense (so that the within-neighbourhood is NeBot at the points which are not isolated on the left), the single-point hypothesis h that f has a within left limit at a, and that f has a within left limit at every point eventually to the left of a.

At a point c which is isolated on the left, leftLimWithin f s c = f c, hence we need those points to belong to s (hypothesis hs'). If the order is densely ordered, there are no such points to the left of a, except possibly a minimal element.

theorem continuousWithinAt_rightLimWithin_Ici_of_dense {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [T3Space β] {f : α → β} {s : Set α} {a : α} (hs : Dense s) (hs' : ∀ᶠ (c : α) in nhdsWithin a (Set.Ioi a), nhdsWithin c (Set.Ioi c) = ⊥ → c ∈ s) (h : Filter.Tendsto f (nhdsWithin a (Set.Ioi a ∩ s)) (nhds (Function.rightLimWithin f s a))) (hlim : ∀ᶠ (c : α) in nhdsWithin a (Set.Ioi a), Filter.Tendsto f (nhdsWithin c (Set.Ioi c ∩ s)) (nhds (Function.rightLimWithin f s c))) : ContinuousWithinAt (Function.rightLimWithin f s) (Set.Ici a) a

Dense version of continuousWithinAt_rightLimWithin_Ici with the stronger conclusion Ici a. The points which are isolated on the right need to belong to s, see continuousWithinAt_leftLimWithin_Iic_of_dense.

theorem leftLimWithin_leftLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [T3Space β] {f : α → β} {s : Set α} {a : α} (h : Filter.Tendsto f (nhdsWithin a (Set.Iio a ∩ s)) (nhds (Function.leftLimWithin f s a))) : Function.leftLimWithin (Function.leftLimWithin f s) s a = Function.leftLimWithin f s a

theorem rightLimWithin_rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [T3Space β] {f : α → β} {s : Set α} {a : α} (h : Filter.Tendsto f (nhdsWithin a (Set.Ioi a ∩ s)) (nhds (Function.rightLimWithin f s a))) : Function.rightLimWithin (Function.rightLimWithin f s) s a = Function.rightLimWithin f s a

theorem leftLimWithin_rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [T3Space β] {f : α → β} {s : Set α} {a : α} [h' : (nhdsWithin a (Set.Iio a ∩ s)).NeBot] (h : Filter.Tendsto f (nhdsWithin a (Set.Iio a ∩ s)) (nhds (Function.leftLimWithin f s a))) : Function.leftLimWithin (Function.rightLimWithin f s) s a = Function.leftLimWithin f s a

theorem rightLimWithin_leftLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [T3Space β] {f : α → β} {s : Set α} {a : α} [h' : (nhdsWithin a (Set.Ioi a ∩ s)).NeBot] (h : Filter.Tendsto f (nhdsWithin a (Set.Ioi a ∩ s)) (nhds (Function.rightLimWithin f s a))) : Function.rightLimWithin (Function.leftLimWithin f s) s a = Function.rightLimWithin f s a

Behaviour at infinity

theorem tendsto_leftLimWithin_atTop_of_tendsto {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [NoTopOrder α] [T3Space β] {f : α → β} {s : Set α} {b : β} (hs : Dense s) (hlim : ∀ (c : α), Filter.Tendsto f (nhdsWithin c (Set.Iio c ∩ s)) (nhds (Function.leftLimWithin f s c))) (h : Filter.Tendsto f Filter.atTop (nhds b)) : Filter.Tendsto (Function.leftLimWithin f s) Filter.atTop (nhds b)

theorem tendsto_rightLimWithin_atTop_of_tendsto {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] [T3Space β] {f : α → β} {s : Set α} {b : β} (hs : Dense s) (hlim : ∀ (c : α), Filter.Tendsto f (nhdsWithin c (Set.Ioi c ∩ s)) (nhds (Function.rightLimWithin f s c))) (h : Filter.Tendsto f Filter.atTop (nhds b)) : Filter.Tendsto (Function.rightLimWithin f s) Filter.atTop (nhds b)

theorem tendsto_rightLimWithin_atBot_of_tendsto {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] [NoBotOrder α] [T3Space β] {f : α → β} {s : Set α} {b : β} (hs : Dense s) (hlim : ∀ (c : α), Filter.Tendsto f (nhdsWithin c (Set.Ioi c ∩ s)) (nhds (Function.rightLimWithin f s c))) (h : Filter.Tendsto f Filter.atBot (nhds b)) : Filter.Tendsto (Function.rightLimWithin f s) Filter.atBot (nhds b)

theorem tendsto_leftLimWithin_atBot_of_tendsto {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [T3Space β] {f : α → β} {s : Set α} {b : β} (hs : Dense s) (hlim : ∀ (c : α), Filter.Tendsto f (nhdsWithin c (Set.Iio c ∩ s)) (nhds (Function.leftLimWithin f s c))) (h : Filter.Tendsto f Filter.atBot (nhds b)) : Filter.Tendsto (Function.leftLimWithin f s) Filter.atBot (nhds b)

theorem Monotone.leftLimWithin_eq_sSup {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} {x : α} [TopologicalSpace α] [OrderTopology α] [(nhdsWithin x (Set.Iio x ∩ s)).NeBot] : Function.leftLimWithin f s x = sSup (f '' Set.Iio x)

For a monotone function, the within left limit is the supremum of the values to the left. Note that the supremum is over the whole Iio x, not just Iio x ∩ s: any subset of Iio x accumulating at x yields the same limit.

theorem Monotone.rightLimWithin_eq_sInf {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} {x : α} [TopologicalSpace α] [OrderTopology α] [(nhdsWithin x (Set.Ioi x ∩ s)).NeBot] : Function.rightLimWithin f s x = sInf (f '' Set.Ioi x)

theorem Monotone.leftLimWithin_le {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} {x y : α} (h : x ≤ y) : Function.leftLimWithin f s x ≤ f y

theorem Monotone.le_leftLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} {x y : α} (h : x < y) : f x ≤ Function.leftLimWithin f s y

theorem Monotone.leftLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} : Monotone (Function.leftLimWithin f s)

theorem Monotone.le_rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} {x y : α} (h : x ≤ y) : f x ≤ Function.rightLimWithin f s y

theorem Monotone.rightLimWithin_le {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} {x y : α} (h : x < y) : Function.rightLimWithin f s x ≤ f y

theorem Monotone.rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} : Monotone (Function.rightLimWithin f s)

theorem Monotone.leftLimWithin_le_rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} {x y : α} (h : x ≤ y) : Function.leftLimWithin f s x ≤ Function.rightLimWithin f s y

theorem Monotone.rightLimWithin_le_leftLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} {x y : α} (h : x < y) : Function.rightLimWithin f s x ≤ Function.leftLimWithin f s y

theorem Monotone.tendsto_leftLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} [TopologicalSpace α] [OrderTopology α] (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Iio x ∩ s)) (nhds (Function.leftLimWithin f s x))

theorem Monotone.tendsto_leftLimWithin_within {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} [TopologicalSpace α] [OrderTopology α] (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Iio x ∩ s)) (nhdsWithin (Function.leftLimWithin f s x) (Set.Iic (Function.leftLimWithin f s x)))

theorem Monotone.tendsto_rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} [TopologicalSpace α] [OrderTopology α] (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x ∩ s)) (nhds (Function.rightLimWithin f s x))

theorem Monotone.tendsto_rightLimWithin_within {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} [TopologicalSpace α] [OrderTopology α] (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x ∩ s)) (nhdsWithin (Function.rightLimWithin f s x) (Set.Ici (Function.rightLimWithin f s x)))

theorem Monotone.continuousWithinAt_Iio_iff_leftLimWithin_eq {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} {x : α} [TopologicalSpace α] [OrderTopology α] : ContinuousWithinAt f (Set.Iio x ∩ s) x ↔ Function.leftLimWithin f s x = f x

A monotone function is continuous to the left within s at x if and only if its within left limit coincides with the value of the function.

theorem Monotone.continuousWithinAt_Ioi_iff_rightLimWithin_eq {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} {x : α} [TopologicalSpace α] [OrderTopology α] : ContinuousWithinAt f (Set.Ioi x ∩ s) x ↔ Function.rightLimWithin f s x = f x

A monotone function is continuous to the right within s at x if and only if its within right limit coincides with the value of the function.

theorem Monotone.continuousWithinAt_iff_leftLimWithin_eq_rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} {x : α} [TopologicalSpace α] [OrderTopology α] : ContinuousWithinAt f s x ↔ Function.leftLimWithin f s x = Function.rightLimWithin f s x

A monotone function is continuous within s at x if and only if its within left and right limits coincide. This is the within-set analogue of continuousAt_iff_leftLim_eq_rightLim, using ContinuousWithinAt f s x in place of the full ContinuousAt f x.

theorem Monotone.continuousAt_iff_leftLimWithin_eq_rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {s : Set α} {x : α} [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] (hs : Dense s) : ContinuousAt f x ↔ Function.leftLimWithin f s x = Function.rightLimWithin f s x

A monotone function is continuous at x (for the full topology) if and only if its within left and right limits along a dense set s coincide. Density is used to recover continuity along the full neighbourhood 𝓝 x from the within-s neighbourhoods.

theorem Antitone.le_leftLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} {x y : α} (h : x ≤ y) : f y ≤ Function.leftLimWithin f s x

theorem Antitone.leftLimWithin_le {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} {x y : α} (h : x < y) : Function.leftLimWithin f s y ≤ f x

theorem Antitone.leftLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} : Antitone (Function.leftLimWithin f s)

theorem Antitone.rightLimWithin_le {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} {x y : α} (h : x ≤ y) : Function.rightLimWithin f s y ≤ f x

theorem Antitone.le_rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} {x y : α} (h : x < y) : f y ≤ Function.rightLimWithin f s x

theorem Antitone.rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} : Antitone (Function.rightLimWithin f s)

theorem Antitone.rightLimWithin_le_leftLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} {x y : α} (h : x ≤ y) : Function.rightLimWithin f s y ≤ Function.leftLimWithin f s x

theorem Antitone.leftLimWithin_le_rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} {x y : α} (h : x < y) : Function.leftLimWithin f s y ≤ Function.rightLimWithin f s x

theorem Antitone.tendsto_leftLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} [TopologicalSpace α] [OrderTopology α] (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Iio x ∩ s)) (nhds (Function.leftLimWithin f s x))

theorem Antitone.tendsto_leftLimWithin_within {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} [TopologicalSpace α] [OrderTopology α] (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Iio x ∩ s)) (nhdsWithin (Function.leftLimWithin f s x) (Set.Ici (Function.leftLimWithin f s x)))

theorem Antitone.tendsto_rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} [TopologicalSpace α] [OrderTopology α] (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x ∩ s)) (nhds (Function.rightLimWithin f s x))

theorem Antitone.tendsto_rightLimWithin_within {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} [TopologicalSpace α] [OrderTopology α] (x : α) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x ∩ s)) (nhdsWithin (Function.rightLimWithin f s x) (Set.Iic (Function.rightLimWithin f s x)))

theorem Antitone.continuousWithinAt_Iio_iff_leftLimWithin_eq {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} {x : α} [TopologicalSpace α] [OrderTopology α] : ContinuousWithinAt f (Set.Iio x ∩ s) x ↔ Function.leftLimWithin f s x = f x

An antitone function is continuous to the left within s at x if and only if its within left limit coincides with the value of the function.

theorem Antitone.continuousWithinAt_Ioi_iff_rightLimWithin_eq {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} {x : α} [TopologicalSpace α] [OrderTopology α] : ContinuousWithinAt f (Set.Ioi x ∩ s) x ↔ Function.rightLimWithin f s x = f x

An antitone function is continuous to the right within s at x if and only if its within right limit coincides with the value of the function.

theorem Antitone.continuousWithinAt_iff_leftLimWithin_eq_rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} {x : α} [TopologicalSpace α] [OrderTopology α] : ContinuousWithinAt f s x ↔ Function.leftLimWithin f s x = Function.rightLimWithin f s x

An antitone function is continuous within s at x if and only if its within left and right limits coincide.

theorem Antitone.continuousAt_iff_leftLimWithin_eq_rightLimWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {s : Set α} {x : α} [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] (hs : Dense s) : ContinuousAt f x ↔ Function.leftLimWithin f s x = Function.rightLimWithin f s x

An antitone function is continuous at x (for the full topology) if and only if its within left and right limits along a dense set s coincide.