Antitone.continuousWithinAt_Iio_iff_leftLim_eq
theorem Antitone.continuousWithinAt_Iio_iff_leftLim_eq :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Antitone f →
∀ {x : α} [inst_4 : TopologicalSpace α] [inst_5 : OrderTopology α],
ContinuousWithinAt f (Set.Iio x) x ↔ Function.leftLim f x = f x
The theorem `Antitone.continuousWithinAt_Iio_iff_leftLim_eq` states that for any function `f` of type `α → β` that is antitone (i.e., a function where an increase in `α` results in a decrease in `β`), and for any given point `x` of type `α`, the function `f` is continuous to the left at this point if and only if the left limit of the function at this point equals the function's value at that point. Here, "continuous to the left" means that the function's value approaches its limit as we approach `x` from values less than `x`, and "left limit" refers to the value the function approaches as the input approaches from the left (values less than `x`). The function `f`, the point `x`, and the limit must all be within a topological space, which provides the concept of closeness or limits. The "left-infinite right-open interval", denoted by `Set.Iio x`, refers to all values less than `x`.
More concisely: For an antitone function `f` from a topological space `α` to a topological space `β` and a point `x` in `α`, `f` is continuous to the left at `x` if and only if the left limit of `f` at `x` equals `f`'s value at `x`.
|
Monotone.countable_not_continuousAt
theorem Monotone.countable_not_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Monotone f →
∀ [inst_4 : TopologicalSpace α] [inst : OrderTopology α] [inst : SecondCountableTopology β],
{x | ¬ContinuousAt f x}.Countable
The theorem `Monotone.countable_not_continuousAt` states that for any ordered and topologically structured types `α` and `β`, where `α` is a linear order and `β` is a conditionally complete linear order with a second countable topology, the set of points at which a monotone function `f` mapping `α` to `β` is not continuous is at most countable. In simpler terms, there can only be countably many discontinuities in a monotone function in a space with a countable base of open sets.
More concisely: A monotone function from a linear order to a conditionally complete, second countable, topologically ordered type with a countable base of open sets has at most a countable number of discontinuities.
|
Antitone.continuousAt_iff_leftLim_eq_rightLim
theorem Antitone.continuousAt_iff_leftLim_eq_rightLim :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Antitone f →
∀ {x : α} [inst_4 : TopologicalSpace α] [inst_5 : OrderTopology α],
ContinuousAt f x ↔ Function.leftLim f x = Function.rightLim f x
The theorem states that for a function `f` from a linearly ordered set `α` to a conditionally complete linearly ordered topological space `β`, the function is antitone (meaning that if `a ≤ b` then `f(b) ≤ f(a)`) if and only if the function is continuous at a point `x` in `α`. This continuity at `x` is equivalent to the left and right limits of the function at `x` being equal. In other words, the value that the function approaches from values less than `x` (the left limit) and the value that the function approaches from values greater than `x` (the right limit) are the same. This guarantees a well-behaved function in most cases.
More concisely: A function from a linearly ordered set to a conditionally complete linearly ordered topological space is antitone if and only if it is continuous at a point, which is equivalent to having equal left and right limits at that point.
|
leftLim_eq_of_eq_bot
theorem leftLim_eq_of_eq_bot :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [hα : TopologicalSpace α]
[h'α : OrderTopology α] (f : α → β) {a : α}, nhdsWithin a (Set.Iio a) = ⊥ → Function.leftLim f a = f a
The theorem `leftLim_eq_of_eq_bot` states that for any two types `α` and `β` such that `α` has a linear order and both `α` and `β` have topological spaces, with `α` also possessing an order topology, and for any function `f` from `α` to `β` and any element `a` of `α`, if the intersection of the set of all elements less than `a` (represented by `Set.Iio a`) and a neighborhood of `a` (represented by `nhdsWithin a (Set.Iio a)`) is the empty set (represented by `⊥`), then the left limit of the function `f` at `a` is equal to the value of the function `f` at `a`. In other words, if `a` has no points immediately to its left, the left limit of `f` at `a` is just `f(a)`.
More concisely: If the set of elements strictly less than a in a linearly ordered type α with an order topology intersects no neighborhood of a in this topology, then the left limit of a function from α to a topological space β at a is equal to f(a).
|
Monotone.le_leftLim
theorem Monotone.le_leftLim :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Monotone f → ∀ {x y : α}, x < y → f x ≤ Function.leftLim f y
The theorem `Monotone.le_leftLim` states that for any types `α` and `β`, given `α` is a linear order, `β` is a conditionally complete linear order and a topological space with an order topology, and a function `f` from `α` to `β` that is monotone, for any elements `x` and `y` of type `α` such that `x` is less than `y`, the value of `f` at `x` is less than or equal to the left limit of `f` at `y`. In mathematical terms, if `f` is a monotone function, then for all `x` and `y` such that `x < y`, we have `f(x) ≤ lim₋ₓ₌y f(x)`.
More concisely: For any monotone function `f` from a linearly ordered type `α` to a conditionally complete linear order and topological space `β` with order topology, if `x` and `y` are in `α` with `x < y`, then `f(x) ≤ lim₋ₓ₌y f(x)`.
|
Antitone.countable_not_continuousAt
theorem Antitone.countable_not_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Antitone f →
∀ [inst_4 : TopologicalSpace α] [inst : OrderTopology α] [inst : SecondCountableTopology β],
{x | ¬ContinuousAt f x}.Countable
This theorem states that in a second countable space, the set of points where an antitone (a function `f` where if `a ≤ b` then `f b ≤ f a`) function is not continuous is at most countable. In other words, for any antitone function `f` mapping from a linearly ordered type `α` to a conditionally complete linearly ordered topological space `β`, if the topology of `β` is second countable, then the set of all points in `α` at which `f` is not continuous is countable. Second countable space refers to a topological space which has a countable base for its topology. Continuous at a point means the function's value tends to the function's value at that point when the input tends to that point.
More concisely: In a second countable linearly ordered topological space, the set of points where an antitone function is discontinuous is countable.
|
Antitone.continuousWithinAt_Ioi_iff_rightLim_eq
theorem Antitone.continuousWithinAt_Ioi_iff_rightLim_eq :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Antitone f →
∀ {x : α} [inst_4 : TopologicalSpace α] [inst_5 : OrderTopology α],
ContinuousWithinAt f (Set.Ioi x) x ↔ Function.rightLim f x = f x
The theorem `Antitone.continuousWithinAt_Ioi_iff_rightLim_eq` states that for any given antitone function `f` from a linearly ordered set `α` to a conditionally complete linearly ordered topological space `β`, the function is continuous to the right at a point `x` if and only if the right limit of the function at `x` is equal to the value of the function at `x`. Here, an antitone function is one where if `a ≤ b`, then `f b ≤ f a`, and continuity to the right at a point within a subset means that `f x` tends to `f x₀` when `x` tends to `x₀` while staying within the subset. The right limit of `f` at `a` is defined by using the order topology on `α`, and if `a` is isolated to its right or the function has no right limit, we use `f a` instead to ensure appropriate behavior in most cases.
More concisely: An antitone function from a linearly ordered set to a conditionally complete linearly ordered topological space is right-continuous at a point if and only if its right limit exists and equals the function value at that point.
|
Monotone.continuousAt_iff_leftLim_eq_rightLim
theorem Monotone.continuousAt_iff_leftLim_eq_rightLim :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Monotone f →
∀ {x : α} [inst_4 : TopologicalSpace α] [inst_5 : OrderTopology α],
ContinuousAt f x ↔ Function.leftLim f x = Function.rightLim f x
The theorem states that for a function `f` mapping from a linear order `α` to a conditionally complete linear order `β`, which are both topological spaces and their corresponding order topologies, the function is monotone if and only if it is continuous at any point `x` in `α`. Furthermore, this continuity at `x` is equivalent to the left and right limits of `f` at `x` being equal. In mathematical terms, a function `f: α → β` is continuous at point `x` if and only if the limit of `f` as it approaches `x` from the left is the same as the limit of `f` as it approaches `x` from the right, assuming that `f` is a monotone function.
More concisely: A monotone function `f: α → β` between two topological linear orders `α` and `β` is continuous at a point `x` if and only if the left and right limits of `f` at `x` are equal.
|
Monotone.continuousWithinAt_Iio_iff_leftLim_eq
theorem Monotone.continuousWithinAt_Iio_iff_leftLim_eq :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Monotone f →
∀ {x : α} [inst_4 : TopologicalSpace α] [inst_5 : OrderTopology α],
ContinuousWithinAt f (Set.Iio x) x ↔ Function.leftLim f x = f x
This theorem states that for a monotone function `f` mapping from a linearly ordered type `α` to a conditionally complete linearly ordered topological space `β`, the function `f` is continuous to the left at a point `x` (meaning within the left-infinite right-open interval ending at `x`) if and only if the left limit of the function at `x` equals the value of the function at `x`. Here, the left limit of a function at a point is the value that the function approaches as it gets arbitrarily close to that point from the left.
More concisely: A monotone function from a linearly ordered type to a conditionally complete linearly ordered topological space is left-continuous at a point if and only if its left limit at that point exists and equals the function value at that point.
|
Monotone.countable_not_continuousWithinAt_Iio
theorem Monotone.countable_not_continuousWithinAt_Iio :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Monotone f →
∀ [inst_4 : TopologicalSpace α] [inst_5 : OrderTopology α] [inst_6 : SecondCountableTopology β],
{x | ¬ContinuousWithinAt f (Set.Iio x) x}.Countable
This theorem states that in a second countable space, the set of points where a monotone function is not left-continuous (i.e., it does not satisfy the property of continuity when approached from the left) is at most countable. This means there exists a one-to-one correspondence between the set of such points and the set of natural numbers, implying these points are countably infinite or finite. The theorem is a special case of a more general theorem `countable_not_continuousAt`, which considers points where the function is not continuous from either side. The theorem applies to a function `f` from a linear order `α` to a conditionally complete linear order `β`, both equipped with a topological space structure and order topology.
More concisely: In a second countable topological space, the set of points where a monotone function from a linearly ordered set to another conditionally complete linearly ordered set is not left-continuous is at most countable.
|
Monotone.leftLim_eq_sSup
theorem Monotone.leftLim_eq_sSup :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Monotone f →
∀ {x : α} [inst_4 : TopologicalSpace α] [inst_5 : OrderTopology α],
nhdsWithin x (Set.Iio x) ≠ ⊥ → Function.leftLim f x = sSup (f '' Set.Iio x)
This theorem states that for every monotone function `f` from a linearly ordered type `α` to a conditionally complete linearly ordered type `β`, both equipped with a topological space structure and an order topology, if the filter of the intersection of the neighborhood within the set of all elements less than `x` and a neighborhood of `x` is not the bottom element, then the left limit of the function `f` at `x` equals the supremum (least upper bound) of the image of the function `f` over the set of all elements less than `x`.
In mathematical terms, if `f` maps each `a ≤ b` to `f a ≤ f b` for all `α` and `β` belonging to the set of real numbers with an order topology, where `x` belongs to `α`, and the intersection of a neighborhood of `x` within the set of numbers less than `x` is not empty, then the left limit of `f` at `x` is equal to the least upper bound of the values of `f` for all inputs less than `x`.
More concisely: If `f` is a monotone function from a linearly ordered type `α` to a conditionally complete linearly ordered type `β`, both with order topologies, and `x` is in `α` such that the intersection of neighborhoods of `x` and elements less than `x` is non-empty, then the left limit of `f` at `x` equals the supremum of `f` over elements less than `x`.
|
Monotone.leftLim_le
theorem Monotone.leftLim_le :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Monotone f → ∀ {x y : α}, x ≤ y → Function.leftLim f x ≤ f y
The theorem `Monotone.leftLim_le` states that for all types `α` and `β`, given that `α` is a linear order, `β` is a conditionally complete linear order, `β` is a topological space, and `β` has an order topology, then for any function `f` from `α` to `β`, if `f` is monotone, i.e., `f` preserves the order (`a ≤ b` implies `f a ≤ f b`), then for all `x` and `y` in `α`, if `x` is less than or equal to `y`, the left limit of the function `f` at `x` is less than or equal to the function `f` at `y`. In other words, the left limit of a monotone function at a point does not exceed the function's value at any greater point.
More concisely: For any monotonic function from a linearly ordered type to a conditionally complete linear order topology, the left limit at a point is less than or equal to the function value at any greater point.
|
Monotone.countable_not_continuousWithinAt_Ioi
theorem Monotone.countable_not_continuousWithinAt_Ioi :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Monotone f →
∀ [inst_4 : TopologicalSpace α] [inst_5 : OrderTopology α] [inst_6 : SecondCountableTopology β],
{x | ¬ContinuousWithinAt f (Set.Ioi x) x}.Countable
The theorem `Monotone.countable_not_continuousWithinAt_Ioi` states that in a second countable space, the set of points where a monotone function is not right-continuous is at most countable. In other words, for any monotone function `f` mapping from a linear ordered type `α` to a conditionally complete linear ordered topological space `β`, the set of all points `x` in `α` such that `f` is not continuous at `x` within the interval `(x, ∞)` is a countable set. This theorem is superseded by `countable_not_continuousAt` which provides a similar result for both left and right continuity.
More concisely: In a second countable space, the set of points where a monotone function is not right-continuous is countable.
|
Monotone.le_rightLim
theorem Monotone.le_rightLim :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Monotone f → ∀ {x y : α}, x ≤ y → f x ≤ Function.rightLim f y
This theorem states that for any two types `α` and `β`, where `α` has a linear order structure, `β` has a conditionally complete linear order and a topological space structure, and `β`'s order and topology are compatible (i.e., `β` is an order topology), given any monotone function `f` from `α` to `β` and any two elements `x` and `y` of `α` with `x ≤ y`, the value of `f` at `x` is less than or equal to the right limit of `f` at `y`. In mathematical terms, if $f: \alpha \rightarrow \beta$ is a monotone function and $x, y$ are elements in $\alpha$ such that $x \leq y$, then $f(x) \leq \lim_{t \rightarrow y^{+}}f(t)$ where the limit is evaluated from the right.
More concisely: For any monotonic function $f: \alpha \to \beta$ between linearly ordered types $\alpha$ and conditionally complete linear order and topological space $\beta$ with compatible order and topology, and for any $x, y \in \alpha$ with $x \leq y$, we have $f(x) \leq \lim\limits_{t \to y^+} f(t)$.
|
Monotone.continuousWithinAt_Ioi_iff_rightLim_eq
theorem Monotone.continuousWithinAt_Ioi_iff_rightLim_eq :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Monotone f →
∀ {x : α} [inst_4 : TopologicalSpace α] [inst_5 : OrderTopology α],
ContinuousWithinAt f (Set.Ioi x) x ↔ Function.rightLim f x = f x
The theorem states that for a function `f` mapping from a linearly ordered type `α` to a conditionally complete linearly ordered topological space `β`, the function is continuous to the right at a point `x` if and only if the right limit of the function at `x` is equal to the function's value at `x`. This is true if the function `f` is monotone. In other words, if the function does not decrease its value when its argument increases (i.e., it is monotone), then the function is continuous from the right at a point if, and only if, the value the function approaches when the argument goes beyond said point (the right limit) is the same as the function's value at that point.
More concisely: For a monotone function `f` from a linearly ordered type `α` to a conditionally complete linearly ordered topological space `β`, continuity to the right at a point `x` is equivalent to the right limit of `f` at `x` being equal to `f(x)`.
|
Monotone.tendsto_leftLim
theorem Monotone.tendsto_leftLim :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Monotone f →
∀ [inst_4 : TopologicalSpace α] [inst_5 : OrderTopology α] (x : α),
Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (Function.leftLim f x))
The theorem `Monotone.tendsto_leftLim` states that for a monotone function `f` from a linear order into a conditionally complete linear order that both have a topological structure compatible with the order (OrderTopology), the function `f` tends to its left limit as we approach any point `x` from the left. In other words, given any point `x` in the domain of `f`, if we consider the sequence of `f` values for points in the left-infinite right-open interval ending at `x` (the set of all points less than `x`), the limit of this sequence is the left limit of `f` at `x`.
More concisely: Given a monotone function `f` from a linearly ordered and conditionally complete topological space into another such space, for any `x` in the domain of `f`, the sequence `{f(y) | y < x}` converges to the left limit of `f` at `x`.
|
Monotone.leftLim
theorem Monotone.leftLim :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
[inst_2 : TopologicalSpace β] [inst_3 : OrderTopology β] {f : α → β},
Monotone f → Monotone (Function.leftLim f)
The theorem `Monotone.leftLim` states that for any types `α` and `β`, where `α` has a Linear Order, `β` has a Conditionally Complete Linear Order, a Topological Space structure, and an Order Topology, if a function `f` from `α` to `β` is Monotone (i.e., if `a ≤ b` implies `f a ≤ f b`), then the left-hand limit function `Function.leftLim f` of `f` is also Monotone.
More concisely: If `f` is a monotonic function from a linearly ordered type `α` to a conditionally complete linearly ordered topological space `β`, then the left-limit function of `f` is also monotonic.
|