StrictMonoOn.continuousWithinAt_right_of_image_mem_nhdsWithin
theorem StrictMonoOn.continuousWithinAt_right_of_image_mem_nhdsWithin :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] [inst_6 : DenselyOrdered β]
{f : α → β} {s : Set α} {a : α},
StrictMonoOn f s →
s ∈ nhdsWithin a (Set.Ici a) → f '' s ∈ nhdsWithin (f a) (Set.Ici (f a)) → ContinuousWithinAt f (Set.Ici a) a
The theorem `StrictMonoOn.continuousWithinAt_right_of_image_mem_nhdsWithin` states that if we have a function `f` from a linearly ordered topological space to a densely ordered topological space, and this function is strictly monotone on a set `s` that is right neighborhood of a point `a`, and if the image of this set under `f` is also a right neighborhood of `f(a)`, then `f` is continuous at the point `a` from the right.
In more mathematical terms, if `f: α → β` is a mapping from a space `α` with a linear order and order topology to a space `β` with a linear order, order topology and dense order, and if `f` is strictly monotone on a set `s` such that `s` is in the intersection of the neighborhood of `a` and the closed-interval [a, ∞), and if the image of `s` under `f` is in the intersection of the neighborhood of `f(a)` and the closed-interval [f(a), ∞), then `f` is continuous at `a` from the right, i.e., for all points in the closed-interval [a, ∞).
More concisely: If a strictly monotone function between linearly ordered and densely ordered topological spaces maps a right neighborhood of a point to another right neighborhood of its image, then the function is continuous at that point from the right.
|
continuousWithinAt_left_of_monotoneOn_of_exists_between
theorem continuousWithinAt_left_of_monotoneOn_of_exists_between :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] {f : α → β} {s : Set α} {a : α},
MonotoneOn f s →
s ∈ nhdsWithin a (Set.Iic a) →
(∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ioo b (f a)) → ContinuousWithinAt f (Set.Iic a) a
The theorem `continuousWithinAt_left_of_monotoneOn_of_exists_between` states that if a function `f` is monotone on a neighborhood to the left of a point `a`, and for every value `b` less than `f(a)`, there exists a point `c` in that neighborhood such that `f(c)` lies strictly between `b` and `f(a)`, then `f` is continuous at `a` from the left. Note that the condition about the existence of such a point `c` cannot be weakened to allow `f(c)` to be equal to `b`, as this would allow discontinuous functions such as the floor function at `a = 0` to be considered.
More concisely: If a function `f` is monotone on a neighborhood to the left of a point `a` and for every `b < f(a)`, there exists a point `c` in that neighborhood with `b < f(c) < f(a)`, then `f` is left-continuous at `a`.
|
Monotone.continuous_of_surjective
theorem Monotone.continuous_of_surjective :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] [inst_6 : DenselyOrdered β]
{f : α → β}, Monotone f → Function.Surjective f → Continuous f
The theorem states that a function `f` from a type `α` to a type `β` is continuous if the following conditions are met:
- `f` is monotone, meaning that for any two elements `a` and `b` of `α`, if `a` is less than or equal to `b`, then `f(a)` is less than or equal to `f(b)`
- `f` is surjective, meaning that for every element `b` of `β`, there exists an element `a` of `α` such that `f(a)` equals `b`
- The types `α` and `β` have a linear order, meaning that for any two elements, one is less than or equal to the other
- The types `α` and `β` have a topology, which gives a notion of 'nearness' of elements
- The order and topology on `α` and `β` are compatible in a specific way (defined by `OrderTopology`)
- The type `β` is densely ordered, meaning that for any two distinct elements, there is another element strictly between them.
More concisely: A function between two ordered and topological types is continuous if it is monotone, surjective, and the order and topology satisfy the OrderTopology and β is densely ordered.
|
StrictMonoOn.continuousWithinAt_left_of_exists_between
theorem StrictMonoOn.continuousWithinAt_left_of_exists_between :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] {f : α → β} {s : Set α} {a : α},
StrictMonoOn f s →
s ∈ nhdsWithin a (Set.Iic a) →
(∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ico b (f a)) → ContinuousWithinAt f (Set.Iic a) a
This theorem states that if we have a function `f` that is strictly monotone on a left neighborhood of a point `a`, and the image of this neighborhood under `f` intersects with every interval `[b, f a)`, where `b < f a`, then `f` is continuous at `a` from the left.
The condition that for every `b < f a`, there exists `c` in the neighborhood such that `f c` lies in the interval `[b, f a)` is necessary to avoid counter-examples like the function `f : ℝ → ℝ` defined by `f x = if x < 0 then x else x + 1` at `a = 0`.
More concisely: If a function `f` is strictly monotone on the left neighborhood of a point `a` and intersects every left interval `(b, fa)` for `b < fa`, then `f` is continuous at `a`.
|
Monotone.continuous_of_denseRange
theorem Monotone.continuous_of_denseRange :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] [inst_6 : DenselyOrdered β]
{f : α → β}, Monotone f → DenseRange f → Continuous f
This theorem states that a function `f` mapping from a type `α` to a type `β` is continuous if the following conditions are met:
- `f` is a monotone function, that is, if for any two elements `a` and `b` in `α` with `a ≤ b`, it holds that `f(a) ≤ f(b)`.
- The codomain `β` is a densely ordered set, meaning that for any two distinct elements `x` and `y` in `β`, there exists an element `z` in `β` such that `x < z < y`.
- The range of `f` is dense in `β`, which means that for any open set `U` in `β`, there is some element `x` from `α` such that `f(x)` is in `U`.
The function `f` is continuous in the topological sense, that is, pre-images of open sets are open.
This theorem involves concepts from order theory and topology.
More concisely: A monotone function `f` from a densely ordered type `α` to a densely ordered and separated topological space `β` with a dense range is continuous if and only if the preimage of every open set in `β` is an open subset of `α`.
|
continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin
theorem continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] [inst_6 : DenselyOrdered β]
{f : α → β} {s : Set α} {a : α},
MonotoneOn f s →
s ∈ nhdsWithin a (Set.Iic a) →
closure (f '' s) ∈ nhdsWithin (f a) (Set.Iic (f a)) → ContinuousWithinAt f (Set.Iic a) a
This theorem states that for a function `f` mapping from a linearly ordered topological space `α` to a linearly ordered topological space `β`, if `f` is monotone on a subset `s` and `s` is within the left neighborhood of `a` (i.e., all elements less than or equal to `a`), and if the closure of the image of `s` under `f` is also within the left neighborhood of `f(a)`, then `f` is continuous at `a` from the left. The "left neighborhood" is defined as all elements less than or equal to a particular value. Both `α` and `β` are densely ordered, meaning between any two different elements, there is another element. The concept of continuity used here is "continuous within at", which means the function is continuous within a given subset at a specified point.
More concisely: If `f` is a monotone function from a densely ordered, linearly topological space `α` to another densely ordered, linearly topological space `β`, and `s` is a subset of `α` within the left neighborhood of `a` such that the closure of `f[s]` is within the left neighborhood of `f(a)`, then `f` is continuous at `a` from the left.
|
StrictMonoOn.continuousWithinAt_right_of_closure_image_mem_nhdsWithin
theorem StrictMonoOn.continuousWithinAt_right_of_closure_image_mem_nhdsWithin :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] [inst_6 : DenselyOrdered β]
{f : α → β} {s : Set α} {a : α},
StrictMonoOn f s →
s ∈ nhdsWithin a (Set.Ici a) →
closure (f '' s) ∈ nhdsWithin (f a) (Set.Ici (f a)) → ContinuousWithinAt f (Set.Ici a) a
This theorem states that if a function `f`, from a linearly ordered type `α` to a densely ordered type `β`, is strictly increasing within a set `s` that lies in the right neighborhood of a point `a` in `α` and the closure of the image of `s` under `f` is in the right neighborhood of the image of `a` under `f`, then `f` is right-continuous at `a`.
Here, the term 'right-continuous at `a`' means that as we approach `a` from values greater than `a` (i.e., from the right side of `a`), the values of the function `f` tend to `f(a)`.
Moreover, the closure of a set is the smallest closed set containing the set, and a 'right neighborhood of a point `a`' refers to an interval of the form `[a, ∞)`. The term 'strictly increasing' means that for any two distinct points in the domain, the value at the larger point is greater than the value at the smaller point.
More concisely: If a strictly increasing function `f` from a linearly ordered type `α` to a densely ordered type `β` is such that the closure of `f`'s image of a right neighborhood of `a` in `α` lies in the right neighborhood of `f(a)` in `β`, then `f` is right-continuous at `a`.
|
StrictMonoOn.continuousWithinAt_left_of_closure_image_mem_nhdsWithin
theorem StrictMonoOn.continuousWithinAt_left_of_closure_image_mem_nhdsWithin :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] [inst_6 : DenselyOrdered β]
{f : α → β} {s : Set α} {a : α},
StrictMonoOn f s →
s ∈ nhdsWithin a (Set.Iic a) →
closure (f '' s) ∈ nhdsWithin (f a) (Set.Iic (f a)) → ContinuousWithinAt f (Set.Iic a) a
The theorem `StrictMonoOn.continuousWithinAt_left_of_closure_image_mem_nhdsWithin` states that if a function `f`, which maps from a linearly ordered type `α` to a densely ordered type `β`, is strictly monotonically increasing on a subset `s` that is a left neighborhood of a point `a` (i.e., the set of all points less than or equal to `a`), and the closure of the image of this subset under `f` is also a left neighborhood of `f(a)`, then the function `f` is continuous at the point `a` from the left. The strict monotonicity of `f` on `s` ensures that for any two points `a` and `b` in `s` where `a` is less than `b`, `f(a)` is less than `f(b)`. The closure of the image of `s` under `f` being a left neighborhood of `f(a)` means that every open set containing `f(a)` also contains almost every value of `f` on `s`. The continuity of `f` at `a` from the left means that the limit of `f` as it approaches `a` from the left equals `f(a)`.
More concisely: If a strictly monotonically increasing function from a linearly ordered type to a densely ordered type is such that the closure of its image of a left neighborhood of a point is also a left neighborhood of the image of that point, then the function is continuous at that point from the left.
|
StrictMonoOn.continuousWithinAt_right_of_surjOn
theorem StrictMonoOn.continuousWithinAt_right_of_surjOn :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] {f : α → β} {s : Set α} {a : α},
StrictMonoOn f s →
s ∈ nhdsWithin a (Set.Ici a) → Set.SurjOn f s (Set.Ioi (f a)) → ContinuousWithinAt f (Set.Ici a) a
The theorem states that if a function `f` is strictly increasing on a set `s` that is a right neighborhood of a point `a` (i.e., the set contains all points greater than or equal to `a`), and the image of this set under `f` includes all points strictly greater than `f(a)`, then `f` is continuous at `a` from the right. In other words, if `f` satisfies these conditions, the limit of `f(x)` as `x` approaches `a` from the right is `f(a)`.
More concisely: If a function `f:` X --> Y is strictly increasing on a right neighborhood of `a` in X and the image of that neighborhood under `f` contains all points strictly greater than `f(a)`, then `f` is continuous at `a`.
|
continuousWithinAt_right_of_monotoneOn_of_exists_between
theorem continuousWithinAt_right_of_monotoneOn_of_exists_between :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] {f : α → β} {s : Set α} {a : α},
MonotoneOn f s →
s ∈ nhdsWithin a (Set.Ici a) →
(∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioo (f a) b) → ContinuousWithinAt f (Set.Ici a) a
The theorem `continuousWithinAt_right_of_monotoneOn_of_exists_between` states that if a function `f` is monotone on a right neighborhood of a point `a`, and the image of this neighborhood under `f` intersects with every interval `(f a, b)` where `b > f a`, then `f` is continuous at `a` from the right. This theorem also notes that the condition `∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioo (f a) b` cannot be weakened to `∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b` (used for strictly monotone functions) because the function `ceil : ℝ → ℤ` would then serve as a counter-example at `a = 0`. In this context, the right neighborhood of `a` is expressed as `Set.Ici a`, which is the set of all elements greater than or equal to `a`, and continuity is defined in terms of the function's behavior within this set.
More concisely: If a function `f` is monotone on the right neighborhood of a point `a` and the image of every right interval `(a, b)` under `f` is non-empty, then `f` is continuous at `a` from the right.
|
StrictMonoOn.continuousWithinAt_left_of_image_mem_nhdsWithin
theorem StrictMonoOn.continuousWithinAt_left_of_image_mem_nhdsWithin :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] [inst_6 : DenselyOrdered β]
{f : α → β} {s : Set α} {a : α},
StrictMonoOn f s →
s ∈ nhdsWithin a (Set.Iic a) → f '' s ∈ nhdsWithin (f a) (Set.Iic (f a)) → ContinuousWithinAt f (Set.Iic a) a
The theorem states that if we have a function `f` mapping from a linearly ordered type `α` to a densely ordered type `β`, and this function is strictly monotonically increasing on a set `s`, then if `s` is within the left neighborhood of a point `a` and the image of `s` under `f` is also within the left neighborhood of `f(a)`, it implies that `f` is continuous at the point `a` from the left. In other words, as `x` approaches `a` from values less than `a`, the function `f(x)` tends to `f(a)`. This continuity is assessed within the left-closed interval up to `a`.
More concisely: If `f` is a strictly monotonically increasing function from a linearly ordered type `α` to a densely ordered type `β`, and `s` is a subset of `α` within the left neighborhood of `a` such that `f(s)` is within the left neighborhood of `f(a)`, then `f` is left-continuous at `a`.
|
StrictMonoOn.continuousWithinAt_right_of_exists_between
theorem StrictMonoOn.continuousWithinAt_right_of_exists_between :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] {f : α → β} {s : Set α} {a : α},
StrictMonoOn f s →
s ∈ nhdsWithin a (Set.Ici a) →
(∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioc (f a) b) → ContinuousWithinAt f (Set.Ici a) a
The theorem `StrictMonoOn.continuousWithinAt_right_of_exists_between` states that for a function `f` of type `α → β`, where both `α` and `β` are linearly ordered and equipped with a topological space and order topology, if `f` is strictly monotone on a set `s`, and `s` is within a neighborhood of `a` which includes all points greater than or equal to `a`, and for all `b` greater than `f(a)`, there exists a `c` in `s` such that `f(c)` lies in the interval `(f a, b]`, then `f` is continuous at `a` from the right.
The condition `∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioc (f a) b` is crucial to avoid counter-examples such as the function `f : ℝ → ℝ` defined by `f x = if x ≤ 0 then x else x + 1` at `a = 0`.
More concisely: If a function `f` between linearly ordered and topological spaces is strictly monotone on a set `s` containing all points greater than or equal to `a`, and for all `b` greater than `f(a)`, there exists `c` in `s` with `f(c)` in the interval `(f a, b]`, then `f` is right-continuous at `a`.
|
continuousWithinAt_right_of_monotoneOn_of_image_mem_nhdsWithin
theorem continuousWithinAt_right_of_monotoneOn_of_image_mem_nhdsWithin :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] [inst_6 : DenselyOrdered β]
{f : α → β} {s : Set α} {a : α},
MonotoneOn f s →
s ∈ nhdsWithin a (Set.Ici a) → f '' s ∈ nhdsWithin (f a) (Set.Ici (f a)) → ContinuousWithinAt f (Set.Ici a) a
The theorem `continuousWithinAt_right_of_monotoneOn_of_image_mem_nhdsWithin` states that if we have a function `f` from a linearly ordered set to a densely ordered set, and this function is monotone on a set `s` that is in the right neighborhood of a point `a` (i.e., all the points of `s` are greater than or equal to `a`), and if the image of this set `s` under `f` is also in the right neighborhood of `f(a)`, then the function `f` is continuous at the point `a` from the right side. In other words, as we approach `a` from values greater than `a`, the function `f` approaches `f(a)`. This result is an important property relating monotonicity and continuity in the context of topological and order spaces.
More concisely: If a function between linearly and densely ordered sets is monotone on a right neighborhood of a point and its image under the function is also in the right neighborhood of the image of that point, then the function is right-continuous at that point.
|
continuousAt_of_monotoneOn_of_image_mem_nhds
theorem continuousAt_of_monotoneOn_of_image_mem_nhds :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] [inst_6 : DenselyOrdered β]
{f : α → β} {s : Set α} {a : α}, MonotoneOn f s → s ∈ nhds a → f '' s ∈ nhds (f a) → ContinuousAt f a
This theorem states that if a function `f` with a densely ordered codomain is monotone on a neighborhood of a point `a`, and the image of this neighborhood under `f` forms a neighborhood of `f(a)`, then `f` is continuous at `a`. Here, 'neighborhood' refers to a set that contains an open set around the given point, 'monotone' means that for any two points in the set, if one is less than or equal to the other, their images under the function also follow the same order, and 'densely ordered' means that for any two distinct points in the codomain, there exists another point between them. The continuity of `f` at `a` is defined by the condition that the limit of `f(x)` as `x` approaches `a` is `f(a)`.
More concisely: If a monotone function `f` with a densely ordered codomain is such that the image of every neighborhood of `a` is a neighborhood of `f(a)`, then `f` is continuous at `a`.
|
continuousWithinAt_left_of_monotoneOn_of_image_mem_nhdsWithin
theorem continuousWithinAt_left_of_monotoneOn_of_image_mem_nhdsWithin :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] [inst_6 : DenselyOrdered β]
{f : α → β} {s : Set α} {a : α},
MonotoneOn f s →
s ∈ nhdsWithin a (Set.Iic a) → f '' s ∈ nhdsWithin (f a) (Set.Iic (f a)) → ContinuousWithinAt f (Set.Iic a) a
The theorem states that if a function `f` is monotone on a set `s` and `s` is contained in the intersection of the left-infinitely right-closed interval centered at `a` and a neighborhood of `a`, and similarly the image of `s` under `f` is contained in the intersection of the left-infinitely right-closed interval centered at `f(a)` and a neighborhood of `f(a)`, then `f` is continuous at `a` from the left. The continuity of `f` at a point `a` from the left means that the limit of `f(x)` as `x` approaches `a` is `f(a)`, where `x` is chosen from the set of values less than or equal to `a`. This theorem is applicable when both the domain and codomain of `f` are equipped with a linear order, a topological space, an order topology, and the codomain is densely ordered.
More concisely: If a monotone function `f` has its domain `s` and image `f[s]` contained in left-infinitely right-closed intervals around `a` and `f(a)`, respectively, in a densely ordered topological space, then `f` is left-continuous at `a`.
|
StrictMonoOn.continuousAt_of_exists_between
theorem StrictMonoOn.continuousAt_of_exists_between :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] {f : α → β} {s : Set α} {a : α},
StrictMonoOn f s →
s ∈ nhds a →
(∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ico b (f a)) →
(∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioc (f a) b) → ContinuousAt f a
This theorem states that if a function `f` is strictly increasing on a neighborhood of a point `a`, and for any value `b` less than `f(a)`, the image of this neighborhood under `f` intersects the interval `[b, f(a))`, and for any `b` greater than `f(a)`, the image intersects the interval `(f(a), b]`, then `f` is continuous at `a`. In other words, if `f` is strictly monotone around `a` and its image around `a` spreads to both the left and right of `f(a)`, then `f` has no jumps or breaks at `a`. This condition provides a kind of local "filling in" property for `f`, ensuring continuity at `a`.
More concisely: If a function `f` is strictly increasing around a point `a` and intersects both the intervals `(-\infty, f(a))` and `(f(a),+\infty)` with the images of neighborhoods of `a`, then `f` is continuous at `a`.
|
StrictMonoOn.continuousAt_of_closure_image_mem_nhds
theorem StrictMonoOn.continuousAt_of_closure_image_mem_nhds :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] [inst_6 : DenselyOrdered β]
{f : α → β} {s : Set α} {a : α},
StrictMonoOn f s → s ∈ nhds a → closure (f '' s) ∈ nhds (f a) → ContinuousAt f a
The theorem states that if a function `f`, which has a densely ordered range, is strictly increasing within a neighborhood of a point `a`, and if the closure of the set obtained by applying `f` to this neighborhood is itself a neighborhood of `f(a)`, then the function `f` is continuous at the point `a`. In simpler terms, if `f` is strictly increasing around `a` and the set of output values around `f(a)` is "dense" enough, then `f` has no jumps or discontinuities at `a`.
More concisely: If a strictly increasing function `f` with a densely ordered range has its range neighborhood of `f(a)` equal to the closure of the image of the neighborhood of `a`, then `f` is continuous at `a`.
|
continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin
theorem continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] [inst_6 : DenselyOrdered β]
{f : α → β} {s : Set α} {a : α},
MonotoneOn f s →
s ∈ nhdsWithin a (Set.Ici a) →
closure (f '' s) ∈ nhdsWithin (f a) (Set.Ici (f a)) → ContinuousWithinAt f (Set.Ici a) a
This theorem states that if we have a function `f` from type `α` to type `β`, where `β` is densely ordered, and this function is monotone on a subset `s` of `α` that lies in the right neighborhood of a point `a` in `α`, then under certain conditions `f` is continuous at `a` from the right. The specific conditions are: the closure of the image of this subset `s` under `f` is itself a right neighborhood of the image of `a` under `f`. In mathematical terms, this theorem deals with the continuity of monotone functions on right neighborhoods using closure of function images and dense orders.
More concisely: If `f` is a monotone function from a dense order `α` to a dense order `β`, and the closure of `f`'s image of a right neighborhood of `a` in `α` contains `f(a)` as an interior point, then `f` is continuous at `a` from the right.
|
continuousAt_of_monotoneOn_of_exists_between
theorem continuousAt_of_monotoneOn_of_exists_between :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] {f : α → β} {s : Set α} {a : α},
MonotoneOn f s →
s ∈ nhds a →
(∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ioo b (f a)) →
(∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioo (f a) b) → ContinuousAt f a
The theorem `continuousAt_of_monotoneOn_of_exists_between` states that if a function `f` is monotone on a neighborhood of a point `a` and for any value `b` less than `f(a)`, there exists a point in the neighborhood whose image under `f` lies in the interval `(b, f(a))` and similarly for any value `b` greater than `f(a)`, there exists a point in the neighborhood whose image under `f` lies in the interval `(f(a), b)`, then the function `f` is continuous at the point `a`. This theorem essentially encapsulates the property of continuity in terms of monotonicity and the existence of certain intermediate values.
More concisely: If a function `f` is monotone on a neighborhood of a point `a` and for all `b` in that neighborhood, there exist points with images `b'` and `b''` such that `b < b' < a < b''`, then `f` is continuous at `a`.
|
StrictMonoOn.continuousWithinAt_left_of_surjOn
theorem StrictMonoOn.continuousWithinAt_left_of_surjOn :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] {f : α → β} {s : Set α} {a : α},
StrictMonoOn f s →
s ∈ nhdsWithin a (Set.Iic a) → Set.SurjOn f s (Set.Iio (f a)) → ContinuousWithinAt f (Set.Iic a) a
The theorem states that if a function `f` (from a linearly ordered topological space to another) is strictly increasing on a left neighborhood `s` of a point `a`, and every value less than `f(a)` is achieved by `f` on `s`, then `f` is continuous on the left of `a`. In other words, if you have a function that is strictly increasing in a neighborhood to the left of a certain point, and that function hits every value less than the function's value at that point within that neighborhood, then you can be sure that the function is left-continuous at that point.
More concisely: If a function between two linearly ordered topological spaces is strictly increasing on a left neighborhood of a point and attains every value less than its value at that point within that neighborhood, then the function is left-continuous at that point.
|
StrictMonoOn.continuousAt_of_image_mem_nhds
theorem StrictMonoOn.continuousAt_of_image_mem_nhds :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] [inst_6 : DenselyOrdered β]
{f : α → β} {s : Set α} {a : α}, StrictMonoOn f s → s ∈ nhds a → f '' s ∈ nhds (f a) → ContinuousAt f a
The theorem `StrictMonoOn.continuousAt_of_image_mem_nhds` states that if we have a function `f` from one topological space to another, where the codomain is densely ordered, and if this function `f` is strictly increasing within some neighborhood (`s`) of a particular point `a`, and the image of this neighborhood under `f` is also a neighborhood of `f(a)`, then the function `f` is continuous at the point `a`. Here, continuity is defined in the topological sense that the function output `f(x)` tends to `f(a)` as `x` tends to `a`. This theorem allows us to infer continuity from the combination of local monotonicity and the nature of the function's map with respect to neighborhoods.
More concisely: If a strictly increasing function `f` on a topological space has its image of a neighborhood of a point `a` that contains `f(a)` as a neighborhood of `f(a)`, then `f` is continuous at `a`.
|
continuousAt_of_monotoneOn_of_closure_image_mem_nhds
theorem continuousAt_of_monotoneOn_of_closure_image_mem_nhds :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α]
[inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [inst_5 : OrderTopology β] [inst_6 : DenselyOrdered β]
{f : α → β} {s : Set α} {a : α}, MonotoneOn f s → s ∈ nhds a → closure (f '' s) ∈ nhds (f a) → ContinuousAt f a
The theorem `continuousAt_of_monotoneOn_of_closure_image_mem_nhds` states that given a function `f` from a linearly ordered type `α` to another linearly ordered type `β`, both equipped with a topological structure and an order topology, if `β` is also densely ordered, then for any set `s` in the neighborhood of a point `a` in `α`, if `f` is monotone on `s`, and the closure of the image of `s` under `f` is in the neighborhood of `f(a)`, then `f` is continuous at `a`. In other words, monotonicity of `f` on a local set and the closure of the image of this set being a local set around the image of the point, ensures the continuity of `f` at this point.
More concisely: If a monotone function between linearly ordered and topologically structured types is such that the closure of its image of a neighborhood of a point is a neighborhood of the image point, then the function is continuous at that point.
|
OrderIso.continuous
theorem OrderIso.continuous :
∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : TopologicalSpace α]
[inst_3 : TopologicalSpace β] [inst_4 : OrderTopology α] [inst_5 : OrderTopology β] (e : α ≃o β), Continuous ⇑e
The theorem `OrderIso.continuous` states that for any two types `α` and `β`, given that `α` and `β` are endowed with a partial order, a topological space structure, and an order topology, any order isomorphism `e` between `α` and `β` is continuous. In other words, if `α` and `β` are topological spaces that have an order topology (a topology based on a partial order), any function that preserves this order is a continuous function.
More concisely: Given types `α` and `β` endowed with a partial order and a topology, any order isomorphism between them is a continuous function.
|