Monotone.Iic
theorem Monotone.Iic :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → Monotone fun x => Set.Iic (f x)
The theorem `Monotone.Iic` states that for any types `α` and `β` with preorder relations, and any monotone function `f` mapping from `α` to `β`, the function `f` remains monotone when mapped to the set of all elements less than or equal to `f(x)`. In other words, if `a ≤ b` in `α`, then the set of all elements less than or equal to `f(a)` is a subset of the set of all elements less than or equal to `f(b)`.
More concisely: For any monotonic function $f$: $\alpha \to \beta$ between preordered types, the image under $f$ of a lower element is an upper bound of its image. In other words, if $a \leq b$ in $\alpha$, then $f(a) \leq f(b)$ and $\{x \in \beta \mid x \leq f(a)\} \subseteq \{x \in \beta \mid x \leq f(b)\}$.
|
Monotone.Iio
theorem Monotone.Iio :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → Monotone fun x => Set.Iio (f x)
The theorem `Monotone.Iio` states that for any two types `α` and `β` equipped with preorder structures, and any function `f` from `α` to `β`, if the function `f` is monotone, then the function that maps each `x` in `α` to the left-infinite right-open interval ending at `f(x)` is also monotone. In mathematical terms, if `f` is a function such that `a ≤ b` implies `f a ≤ f b` for all `a` and `b` in `α`, then for all `x` in `α`, the set of all `y` in `α` such that `y < f(x)` is a monotone function of `x`.
More concisely: If `f` is a monotone function from preorder types `α` to `β`, then the function mapping each `x` in `α` to the left-open interval `(-\infty, f(x))` is also monotone.
|
StrictMonoOn.Iic_id_le
theorem StrictMonoOn.Iic_id_le :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] [inst_3 : OrderBot α]
{n : α} {φ : α → α}, StrictMonoOn φ (Set.Iic n) → ∀ m ≤ n, m ≤ φ m
The theorem `StrictMonoOn.Iic_id_le` states that for any type `α` that has a partial order, a successor order, is succ-archimedean, and has a bottom element, and for any function `φ` that is strictly monotone on the left-infinite, right-closed interval (`Set.Iic`) up to a given value `n`, then for any `m` that is less than or equal to `n`, `m` is always less than or equal to `φ(m)`. In simpler terms, for any number `m` up to `n`, applying the function `φ` will either increase `m` or leave it the same, but never decrease it.
More concisely: For any strictly monotone function `φ` on the left-infinite, right-closed interval of a succ-archimedean type with bottom element, `m` is less than or equal to `φ(m)` for all `m` less than or equal to the given value `n`.
|
strictMonoOn_Iic_of_lt_succ
theorem strictMonoOn_Iic_of_lt_succ :
∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] {ψ : α → β} [inst_2 : SuccOrder α]
[inst_3 : IsSuccArchimedean α] {n : α}, (∀ m < n, ψ m < ψ (Order.succ m)) → StrictMonoOn ψ (Set.Iic n)
The theorem `strictMonoOn_Iic_of_lt_succ` asserts that for any `SuccOrder` (an order where every element has a successor) on an arbitrary type `α`, and a function `ψ` from `α` to another arbitrary type `β`, if for all `m` less than a given `n`, the value of `ψ` at `m` is less than the value of `ψ` at the successor of `m`, then `ψ` is strictly monotone on the interval of `α` that includes all elements less than or equal to `n`. In other words, `ψ` increases as you move up in the order from any point to its successor, up to the point `n`.
More concisely: If `ψ : α → β` is a function on a type `α` with a `SuccOrder`, and `ψ` is decreasing on all intervals `[m, succ m]` for all `m` less than some `n`, then `ψ` is strictly increasing on the interval `[min α, n]`.
|
antitone_Ici
theorem antitone_Ici : ∀ {α : Type u_1} [inst : Preorder α], Antitone Set.Ici
The theorem `antitone_Ici` states that for any preorder set `α`, the function `Set.Ici`, which produces left-closed right-infinite intervals, is antitone. In other words, if `a ≤ b` for any two elements `a` and `b` in the set `α`, then the interval starting from `b` is a subset of the interval starting from `a`.
More concisely: For any preorder set α, the function Set.Ici returns left-closed right-infinite intervals, and these intervals are antitone, meaning that for all a ≤ b in α, the interval [a, ∞[ (Ici a) is contained in the interval [b, ∞[ (Ici b).
|
monotone_Iio
theorem monotone_Iio : ∀ {α : Type u_1} [inst : Preorder α], Monotone Set.Iio
The theorem `monotone_Iio` states that for any type `α` that has a preorder (a binary relation that is both reflexive and transitive), the function `Set.Iio` is monotone. In other words, if we have two elements `a` and `b` of type `α` such that `a` is less than or equal to `b`, then the left-infinite right-open interval ending at `a` is a subset of the left-infinite right-open interval ending at `b`. This can be written in mathematical notation as: for all `a` and `b` in `α`, if `a ≤ b` then `{x | x < a} ⊆ {x | x < b}`.
More concisely: For any type `α` with a preorder, the function `Set.Iio` maps smaller elements to smaller sets: `{x | x < a} ⊆ {x | x < b}` when `a ≤ b`.
|
antitone_Ioi
theorem antitone_Ioi : ∀ {α : Type u_1} [inst : Preorder α], Antitone Set.Ioi
The theorem `antitone_Ioi` states that for all types `α` that have a preorder (an order relation that is reflexive and transitive), the function `Set.Ioi` (which creates a set of all elements greater than a given element in `α`) is antitone. In other words, if `a ≤ b` for two elements `a` and `b` in `α`, then the set of elements greater than `b` is a subset of the set of elements greater than `a`. This is expressed by saying that the set of elements greater than `b` is less than or equal to the set of elements greater than `a` in the order relation of sets, which is set inclusion.
More concisely: For any preorder `≤` on type `α`, the set `Set.Ioi a` is a subset of `Set.Ioi b` whenever `a ≤ b`.
|
monotone_Iic
theorem monotone_Iic : ∀ {α : Type u_1} [inst : Preorder α], Monotone Set.Iic
The theorem `monotone_Iic` states that for any type `α` with a preorder structure, the function `Set.Iic` is monotone. In other words, if `a ≤ b` for some `a` and `b` of type `α`, then the set of all elements less than or equal to `a` is a subset of the set of all elements that are less than or equal to `b`. This is the mathematical way of saying that the interval "up to `a`" is contained in the interval "up to `b`" when `a` is less than or equal to `b`.
More concisely: For any preordered type `α`, the set inclusion `Set.Iic a ⊆ Set.Iic b` holds when `a ≤ b`.
|
Antitone.Ioi
theorem Antitone.Ioi :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Antitone f → Monotone fun x => Set.Ioi (f x)
The theorem `Antitone.Ioi` states that for all types `α` and `β` that have a preorder (a binary relation that is reflexive and transitive), if there exists an antitone function `f` from `α` to `β`, then the function that maps `x` to the set of all elements in `α` that are strictly greater than `f(x)` is a monotone function. In other words, if `f` is a function that decreases or remains constant as its input increases (antitone), then the function that forms an open interval of values greater than the output of `f` increases or remains constant as its input increases (monotone).
More concisely: If `f` is an antitone function between preordered types `α` and `β`, then the function mapping each `x` in `α` to the set of elements strictly greater than `f(x)` is monotone.
|