StrictMonoOn.Iic_union_Ici
theorem StrictMonoOn.Iic_union_Ici :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {a : α} {f : α → β},
StrictMonoOn f (Set.Iic a) → StrictMonoOn f (Set.Ici a) → StrictMono f
The theorem `StrictMonoOn.Iic_union_Ici` states that for any type `α` with a linear order, type `β` with a preorder, a value `a` of type `α`, and a function `f` from `α` to `β`, if `f` is strictly increasing on the interval from negative infinity to `a` inclusive (`(-∞, a]`), and `f` is also strictly increasing on the interval from `a` to positive infinity inclusive (`[a, ∞)`), then `f` is strictly increasing everywhere. This theorem essentially says that if a function is strictly increasing on two adjacent intervals that cover the entire real line, then it is strictly increasing on the entire line.
More concisely: If a function from a linearly ordered type to a preordered type is strictly increasing on both the interval from negative infinity to a given element and the interval from that element to positive infinity, then it is strictly increasing on the entire domain.
|
StrictAntiOn.Iic_union_Ici
theorem StrictAntiOn.Iic_union_Ici :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {a : α} {f : α → β},
StrictAntiOn f (Set.Iic a) → StrictAntiOn f (Set.Ici a) → StrictAnti f
The theorem states that if a function `f` which maps from a linearly ordered type `α` to a preordered type `β` is strictly antitone (meaning for any two elements `a` and `b` where `a < b`, it always holds that `f(b) < f(a)`) on the intervals `(-∞, a]` and `[a, ∞)`, then this function `f` is strictly antitone on the entire real line.
In other words, if the function `f` decreases in value as its input increases for all inputs less than or equal to `a` and for all inputs greater than or equal to `a`, then the function `f` decreases in value as its input increases for all possible inputs.
More concisely: If a function `f` strictly decreases on the intervals `(-\infty, a]` and `[a, +\infty)` in a linearly ordered type, then it is strictly antitone on the entire real line.
|
StrictMonoOn.union
theorem StrictMonoOn.union :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α} {c : α},
StrictMonoOn f s → StrictMonoOn f t → IsGreatest s c → IsLeast t c → StrictMonoOn f (s ∪ t)
The theorem `StrictMonoOn.union` states that for any two sets `s` and `t` of a linearly ordered type `α`, and a function `f` mapping from `α` to a preordered type `β`, if `f` is strictly increasing on both `s` and `t`, with `s` being to the left of `t` (in terms of the linear order) and a common element `c` being the greatest element of `s` and the least element of `t`, then `f` is strictly increasing on the union of `s` and `t`. This means that for all pairs of elements in the union of `s` and `t`, if the first element is less than the second, then the result of applying `f` to the first element is less than the result of applying `f` to the second. The monotonicity property of `f` is preserved across the union of the two sets.
More concisely: If functions $f:\alpha \to \beta$ are strictly increasing on disjoint, linearly ordered sets $s,t \subseteq \alpha$ with a common element $c$ being their greatest element in $s$ and least element in $t$, then $f$ is strictly increasing on their union.
|
StrictAntiOn.union
theorem StrictAntiOn.union :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α} {c : α},
StrictAntiOn f s → StrictAntiOn f t → IsGreatest s c → IsLeast t c → StrictAntiOn f (s ∪ t)
The theorem `StrictAntiOn.union` states that if a function `f` is strictly decreasing on two sets `s` and `t` in a linear order space, and `s` is to the left of `t` with a center point `c` belonging to both `s` and `t`, then the function `f` is strictly decreasing on the union of `s` and `t`. Here, `StrictAntiOn f s` and `StrictAntiOn f t` are used to represent that `f` is strictly decreasing on `s` and `t` respectively. The terms `IsGreatest s c` and `IsLeast t c` imply that `c` is the greatest element in `s` and the least element in `t`.
More concisely: If a function `f` is strictly decreasing on sets `s` and `t` in a linear order space, with `s` to the left of `t` and their common point `c` being the greatest element in `s` and the least element in `t`, then `f` is strictly decreasing on the union of `s` and `t`.
|
MonotoneOn.Iic_union_Ici
theorem MonotoneOn.Iic_union_Ici :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {a : α} {f : α → β},
MonotoneOn f (Set.Iic a) → MonotoneOn f (Set.Ici a) → Monotone f
The theorem `MonotoneOn.Iic_union_Ici` states that if a function `f` is monotone on two intervals: `(-∞, a]` and `[a, ∞)`, where `a` is any real number, then `f` is monotone on the entire real line. In other words, if for all `a` and `b` within each of the two intervals, if `a` is less than or equal to `b`, then `f(a)` is less than or equal to `f(b)`, then for any `a` and `b` in the real line, if `a` is less than or equal to `b`, then `f(a)` is less than or equal to `f(b)`. This theorem requires that the domain of `f` has a linear order and the codomain of `f` has a preorder.
More concisely: If a function `f` is monotone on both the left open and right closed intervals of a real number `a`, then `f` is monotone on the entire real line.
|
AntitoneOn.union_right
theorem AntitoneOn.union_right :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α} {c : α},
AntitoneOn f s → AntitoneOn f t → IsGreatest s c → IsLeast t c → AntitoneOn f (s ∪ t)
The theorem `AntitoneOn.union_right` states that if a function `f` is antitone (i.e., it preserves the reverse of the order) on two sets `s` and `t`, with `s` preceding `t` and a common element `c` being the greatest element in `s` and the least in `t`, then the function `f` is also antitone on the union of `s` and `t`. Here, being antitone on a set means that for all elements `a` and `b` in the set, if `a` is less than or equal to `b`, then the value of the function `f` at `b` is less than or equal to the function `f` at `a`. The types `α` and `β` are equipped with a linear order and a preorder structure respectively.
More concisely: If functions $f$ is antitone on sets $s$ and $t$ with a common element $c$ being their greatest element in $s$ and least element in $t$, then $f$ is antitone on the union of $s$ and $t$.
|
AntitoneOn.Iic_union_Ici
theorem AntitoneOn.Iic_union_Ici :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {a : α} {f : α → β},
AntitoneOn f (Set.Iic a) → AntitoneOn f (Set.Ici a) → Antitone f
The theorem `AntitoneOn.Iic_union_Ici` states that if a function `f` is antitone on the intervals `(-∞, a]` and `[a, ∞)`, then it is also antitone over the whole real line. Here, `f` being antitone means that if `a ≤ b`, then `f(b) ≤ f(a)`. The intervals `(-∞, a]` and `[a, ∞)` represent all real numbers less than or equal to `a`, and all real numbers greater than or equal to `a`, respectively.
More concisely: If a function `f` is antitone on both the intervals `(-∞, a]` and `[a, ∞)`, then it is antitone on the whole real line.
|
MonotoneOn.union_right
theorem MonotoneOn.union_right :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α} {c : α},
MonotoneOn f s → MonotoneOn f t → IsGreatest s c → IsLeast t c → MonotoneOn f (s ∪ t)
The theorem `MonotoneOn.union_right` states that given a function `f` from type `α` to type `β`, where `α` has a linear order and `β` has a preorder, and given two sets `s` and `t` of elements of the type `α`. If `f` is monotone on both sets `s` and `t`, with `s` having elements lesser than or equal to a center point `c` (i.e., `c` is the greatest element of `s`) and `t` having elements greater than or equal to `c` (i.e., `c` is the least element of `t`), then `f` is also monotone on the union of sets `s` and `t`. In more mathematical terms, if `f` preserves the order when moving from smaller to larger elements in both `s` and `t`, then it will also preserve the order when moving from smaller to larger elements in `s ∪ t`.
More concisely: If functions `f` from a linearly ordered type `α` to a preordered type `β` are monotone on disjoint sets `s` and `t` with `s` less than or equal to a center point `c` and `t` greater than or equal to `c`, then `f` is monotone on their union `s ∪ t`.
|