monotone_id
theorem monotone_id : ∀ {α : Type u} [inst : Preorder α], Monotone id
The theorem `monotone_id` states that for any type `α` that has a preorder (a binary relation reflecting a linearity/ordering of some kind), the identity function on this type is monotone. In other words, for all `a` and `b` in `α`, if `a` is less than or equal to `b`, then `id a` (which is just `a`) is less than or equal to `id b` (which is just `b`). This is essentially a formalization of the obvious fact that the identity function preserves the order of elements in any ordered set.
More concisely: For any type equipped with a preorder, the identity function is a monotone function with respect to the preorder relation.
|
StrictAnti.lt_iff_lt
theorem StrictAnti.lt_iff_lt :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
StrictAnti f → ∀ {a b : α}, f a < f b ↔ b < a
This theorem states that for any types `α` and `β`, where `α` has a linear order and `β` has a preorder, if a function `f` from `α` to `β` is strictly anti-tonic (i.e., `a < b` implies `f(b) < f(a)`), then for any two elements `a` and `b` of `α`, `f(a) < f(b)` if and only if `b < a`.
More concisely: For any types `α` with a linear order and `β` with a preorder, a strictly anti-tonic function `f` from `α` to `β` satisfies `a < b` if and only if `f(a) < f(b)` if and only if `b < a`.
|
StrictMono.id_le
theorem StrictMono.id_le : ∀ {φ : ℕ → ℕ}, StrictMono φ → ∀ (n : ℕ), n ≤ φ n
The theorem `StrictMono.id_le` states that for all functions `φ` from natural numbers to natural numbers, if `φ` is strictly monotone (i.e., for any two natural numbers `a` and `b` such that `a < b`, `φ(a) < φ(b)`), then for any natural number `n`, `n` is less than or equal to `φ(n)`. This implies that a strictly monotone function on natural numbers always maps a number to itself or a larger number.
More concisely: If `φ` is a strictly monotone function from natural numbers to natural numbers, then for all `n`, `n ≤ φ(n)`.
|
StrictMono.dual_right
theorem StrictMono.dual_right :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
StrictMono f → StrictAnti (⇑OrderDual.toDual ∘ f)
The theorem `StrictMono.dual_right` states that for all types `α` and `β`, that have preorders defined on them, and for any function `f` from `α` to `β`, if `f` is strictly monotone, then the composition of `f` with the function `OrderDual.toDual` (which maps each element to its order dual) is strictly antitone. In simpler terms, if a function `f` strictly increases as its input increases, then when we look at the function under the "dual" ordering (which is the reverse of the initial ordering), the new function strictly decreases as its input increases.
More concisely: If `f : α → β` is strictly monotone between preordered types `α` and `β`, then `OrderDual.toDual ∘ f` is strictly antitone.
|
Monotone.reflect_lt
theorem Monotone.reflect_lt :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → ∀ {a b : α}, f a < f b → a < b
The theorem `Monotone.reflect_lt` states that for any types `α` and `β`, given a linear order structure on `α` and a preorder structure on `β`, if a function `f` from `α` to `β` is monotone (that is, `f` preserves the order), then for any two elements `a` and `b` of `α`, if `f(a)` is less than `f(b)`, it implies that `a` is less than `b`. In other words, a monotone function reflects the 'less than' relation from its codomain to its domain.
More concisely: If `f: α → β` is a monotone function between linearly ordered types `α` and `β` with preorder relation, then `a < b` in `α` implies `f(a) < f(b)` in `β`.
|
monotone_comp_ofDual_iff
theorem monotone_comp_ofDual_iff :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone (f ∘ ⇑OrderDual.ofDual) ↔ Antitone f
This theorem states that for any two types `α` and `β` that have preorder structures, for any function `f` from `α` to `β`, the function `f` composed with the identity function of the dual order of `α` is monotone if and only if the function `f` is antitone. In other words, `f` is increasing when applied after the dual order identity if and only if `f` is decreasing when applied on its own.
More concisely: For types `α` and `β` with preorders, function `f` from `α` to `β` is monotone with respect to the dual orders if and only if `f` is antitone.
|
StrictMonoOn.lt_iff_lt
theorem StrictMonoOn.lt_iff_lt :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictMonoOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → (f a < f b ↔ a < b)
This theorem states that for any two types `α` and `β`, where `α` is a linear order and `β` is a preorder, and for any function `f` from `α` to `β` and any set `s` of type `α`, if `f` is strictly monotonic on `s`, then for all `a` and `b` in `s`, `f(a)` is less than `f(b)` if and only if `a` is less than `b`. In other words, a strictly monotonic function preserves the order of its inputs in the set.
More concisely: If `f` is a strictly monotonic function from a linear order `α` to a preorder `β`, then `a < b` in `α` implies `f(a) < f(b)` in `β`.
|
strictAnti_comp_ofDual_iff
theorem strictAnti_comp_ofDual_iff :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
StrictAnti (f ∘ ⇑OrderDual.ofDual) ↔ StrictMono f
This theorem states that for any two types `α` and `β` with preorder structures and a function `f` from `α` to `β`, the function `f` is strictly monotone if and only if the composition of `f` with the identity function on the `OrderDual` of `α` is strictly antitone.
In other words, a function `f` is strictly increasing (`StrictMono`) if reversing the order of its input (`OrderDual.ofDual`) makes it strictly decreasing (`StrictAnti`). So, if you reverse the order of the inputs, and the order of the outputs also gets reversed, then the original function was strictly increasing. This theorem establishes the connection between strict monotonicity and strict anti-monotonicity under the effect of dual ordering.
More concisely: For functions between preordered types, a function is strictly monotone if and only if the reverse function composed with the order dual is strictly antitone.
|
Monotone.comp
theorem Monotone.comp :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
{f : α → β}, Monotone g → Monotone f → Monotone (g ∘ f)
The theorem `Monotone.comp` states that, for any three types `α`, `β`, and `γ` which are all preordered, if `g` is a function from `β` to `γ` and `f` is a function from `α` to `β`, then if `g` and `f` are both monotone (i.e., if `a ≤ b` then `f a ≤ f b` and if `x ≤ y` then `g x ≤ g y`), then the composition of `g` and `f` is also monotone. That is, for any `a` and `b` in `α`, if `a ≤ b` then `(g ∘ f) a ≤ (g ∘ f) b`.
More concisely: If `f: α → β` and `g: β → γ` are monotone functions between preordered types, then their composition `g ∘ f: α → γ` is also a monotone function.
|
StrictAnti.injective
theorem StrictAnti.injective :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
StrictAnti f → Function.Injective f
The theorem `StrictAnti.injective` states that for any types `α` and `β` with a linear order on `α` and a preorder on `β`, if a function `f` from `α` to `β` is strictly antitone (i.e., if `a` is less than `b` then `f(b)` is less than `f(a)`), then `f` is also injective (i.e., if `f(x)` is equal to `f(y)` then `x` is equal to `y`).
More concisely: If `f` is a strictly antitone function from a linearly ordered type `α` to a preordered type `β`, then `f` is injective.
|
Monotone.dual_left
theorem Monotone.dual_left :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → Antitone (f ∘ ⇑OrderDual.ofDual)
**Monotone.dual_left Theorem**: For any types `α` and `β` that are preordered, and for any function `f` from `α` to `β`, if `f` is monotone, then the composition of `f` with the identity function on the dual order of `α` is antitone. This means that if `f` preserves the order of `α` (i.e., `f` is monotone), then when applied to the dual order of `α`, `f` reverses the order (i.e., becomes antitone). The dual order of `α` is simply `α` with the order reversed.
More concisely: If `f` is a monotone function from preordered types `α` to `β`, then `f` composed with the reverse order function on `α` is an antitone function.
|
strictMono_id
theorem strictMono_id : ∀ {α : Type u} [inst : Preorder α], StrictMono id
The theorem `strictMono_id` asserts that for every type `α`, given that `α` has a preorder relation, the identity function on `α` is strictly monotone. In other words, it means that if `a` and `b` are elements of `α` such that `a < b`, then `id a < id b`, which is the same as `a < b`. Thus, the identity function preserves the order in a set with a preorder.
More concisely: If `α` is a type with a preorder relation, then the identity function on `α` is a strict monotone function with respect to this preorder.
|
antitone_comp_ofDual_iff
theorem antitone_comp_ofDual_iff :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Antitone (f ∘ ⇑OrderDual.ofDual) ↔ Monotone f
This theorem states that for any types `α` and `β` with preorders, and any function `f` from `α` to `β`, the function `f` composed with the order-dual identity function is antitone if and only if the function `f` is monotone. In other words, reversing the order of the arguments of `f` results in an antitone function if and only if `f` itself is monotone. This highlights the relationship between monotone and antitone functions: the former preserves the order of elements while the latter reverses it.
More concisely: For functions between preordered types, `f : α → β` is antitone if and only if its order-dual `dual f` is monotone, where `dual f(x) := f(x) <= f(y) <-> y <= x`.
|
StrictMono.monotone
theorem StrictMono.monotone :
∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β}, StrictMono f → Monotone f
The theorem `StrictMono.monotone` states that for any types `α` and `β`, which have a partial order and preorder respectively, and any function `f` from `α` to `β`, if `f` is strictly monotone, then `f` is also monotone. In other words, if for all `a` and `b` in `α` such that `a < b` it holds that `f(a) < f(b)`, then it must also be the case that for all `a` and `b` in `α` such that `a ≤ b`, we have `f(a) ≤ f(b)`.
More concisely: If `f` is a strictly monotonic function from a partially ordered type `α` to a preordered type `β`, then `f` is monotonic.
|
strictMono_toDual_comp_iff
theorem strictMono_toDual_comp_iff :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
StrictMono (⇑OrderDual.toDual ∘ f) ↔ StrictAnti f
This theorem states that for any two types `α` and `β` with preorder relations (i.e., they are partially ordered sets where every two elements are comparable), and given a function `f` from `α` to `β`, the function `f` is strictly anti-monotone (i.e., `f` reverses the order: if `a < b` then `f(b) < f(a)`) if and only if the function obtained by composing `f` with the identity on the order dual of `α` is strictly monotone (i.e., `f` preserves the order: if `a < b` then `f(a) < f(b)`). In other words, when we reverse the order in the domain, a strictly monotone function becomes strictly anti-monotone, and vice versa.
More concisely: For any functions between partially ordered sets, a function is strictly anti-monotone if and only if the function composed with the order dual's identity is strictly monotone.
|
AntitoneOn.dual_right
theorem AntitoneOn.dual_right :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
AntitoneOn f s → MonotoneOn (⇑OrderDual.toDual ∘ f) s
The theorem `AntitoneOn.dual_right` states that for any two types `α` and `β` that have the structure of a preorder, any function `f` from `α` to `β`, and any set `s` of `α`, if `f` is antitone on `s` (that is, for all `a` and `b` in `s`, `a ≤ b` implies `f(b) ≤ f(a)`), then the composition of `f` with the `toDual` function (which gives the dual order) is monotone on `s` (that is, for all `a` and `b` in `s`, `a ≤ b` implies `f(Dual(a)) ≤ f(Dual(b))`). In other words, applying the `toDual` function to an antitone function results in a monotone function.
More concisely: If `f: α → β` is an antitone function between preordered types `α` and `β`, then the composition `f ∘ toDual` is a monotone function.
|
Nat.exists_strictMono'
theorem Nat.exists_strictMono' :
∀ {α : Type u} [inst : Preorder α] [inst_1 : NoMaxOrder α] (a : α), ∃ f, StrictMono f ∧ f 0 = a
This theorem states that if `α` is a type with a preorder structure and it has no maximal elements (i.e., for any element, there is always another element that is larger), then for any given element `a` in `α`, there exists a strictly monotone function from the natural numbers `ℕ` to `α` such that the function's value at zero is `a`. In other words, we can always find a function that maps the natural numbers into `α` in strictly increasing order starting from any point.
More concisely: If `α` is a preordered type without maximal elements, then for every `a` in `α`, there exists a strictly monotone function `f : ℕ → α` with `f 0 = a`.
|
StrictMono.comp_strictMonoOn
theorem StrictMono.comp_strictMonoOn :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
{f : α → β} {s : Set α}, StrictMono g → StrictMonoOn f s → StrictMonoOn (g ∘ f) s
The theorem `StrictMono.comp_strictMonoOn` states that for any types `α`, `β`, and `γ` that have a pre-order relation, if `g` is a strictly monotonic function from `β` to `γ`, and `f` is a strictly monotonic function on a set `s` of `α`, then the composition function `(g ∘ f)` is also strictly monotonic on the same set `s`. In other words, the composition of a strictly monotonic function and a function that is strictly monotonic on a certain set inherits the strict monotonicity on this set.
More concisely: If `f` is strictly monotonic on a set `s` of `α` and `g` is a strictly monotonic function from `β` to `γ`, then the composition `(g ∘ f)` is strictly monotonic on `s`.
|
Nat.exists_strictMono
theorem Nat.exists_strictMono :
∀ (α : Type u) [inst : Preorder α] [inst_1 : Nonempty α] [inst_2 : NoMaxOrder α], ∃ f, StrictMono f
The theorem states that if we have a type `α` which satisfies three conditions - it is nonempty, it is a preorder (meaning it has a binary relation that is reflexive and transitive), and it does not have any maximal elements - then we can guarantee the existence of a strictly monotone function from the set of natural numbers `ℕ` to `α`. In other words, there is a function such that for any two different natural numbers `a` and `b`, if `a` is less than `b`, then the function evaluated at `a` is less than the function evaluated at `b` in the preorder `α`.
More concisely: If `α` is a nonempty preorder type without maximal elements, then there exists a strictly monotone function from `ℕ` to `α`.
|
StrictAnti.dual
theorem StrictAnti.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
StrictAnti f → StrictAnti (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
The theorem `StrictAnti.dual` states that for any preorder types `α` and `β`, and any function `f` from `α` to `β`, if `f` is strictly antitone (meaning, if `a < b` then `f(b) < f(a)`), then the function obtained by first applying `OrderDual.ofDual` to the argument, then applying `f`, and finally applying `OrderDual.toDual` to the result, is also strictly antitone. In other words, the ordering-reversing operations `OrderDual.ofDual` and `OrderDual.toDual` preserve the property of being strictly antitone.
More concisely: If `f` is a strictly antitone function between preorders `α` and `β`, then `OrderDual.toDual ∘ f ∘ OrderDual.ofDual` is also strictly antitone.
|
not_monotone_not_antitone_iff_exists_lt_lt
theorem not_monotone_not_antitone_iff_exists_lt_lt :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
The theorem `not_monotone_not_antitone_iff_exists_lt_lt` states that for any function `f` mapping from one linearly ordered type `α` to another `β`, the function is neither a monotone function nor an antitone function if and only if there exist three elements `a`, `b`, and `c` in `α` such that `a` is less than `b`, `b` is less than `c`, and either `f(a)` is less than `f(b)` and `f(c)` is less than `f(b)`, or `f(b)` is less than `f(a)` and `f(b)` is less than `f(c)`. In simple terms, the theorem says that a function is not monotone and not antitone if and only if it makes a 'dent' in the order, either 'upright' or 'downright'.
More concisely: A function between linearly ordered types is neither monotone nor antitone if and only if there exist elements a < b < c such that either f(a) < f(b) < f(c) or f(b) < f(a) < f(c).
|
AntitoneOn.dual_left
theorem AntitoneOn.dual_left :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
AntitoneOn f s → MonotoneOn (f ∘ ⇑OrderDual.ofDual) s
The theorem `AntitoneOn.dual_left` states that for any type `α` and `β` that are preordered, along with a function `f` from `α` to `β` and a set `s` of type `α`, if the function `f` is antitone on `s`, then the function obtained by composing `f` with the dual of the order on `α` is monotone on `s`. In simpler terms, if `f` is a function that decreases or remains constant with increasing input in `s`, then when the order of the inputs is reversed, `f` becomes a function that increases or remains constant with increasing input in `s`.
More concisely: If `f` is an antitone function from a preordered type `α` to another preordered type `β` on a set `s`, then the composite function `dual_α ∘ f` is monotone on `s`, where `dual_α` is the dual ordering on `α`.
|
Monotone.comp_antitone
theorem Monotone.comp_antitone :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
{f : α → β}, Monotone g → Antitone f → Antitone (g ∘ f)
The theorem `Monotone.comp_antitone` states that for any three types `α`, `β`, and `γ`, which have the preorder relation, and any two functions `g : β → γ` and `f : α → β`, if `g` is a monotone function and `f` is an antitone function, then the composition of `g` and `f` (i.e., `g ∘ f`) is an antitone function. In other words, if the function `g` preserves order and the function `f` reverses order, then their composition also reverses order.
More concisely: If `f : α → β` is antitone and `g : β → γ` is monotone, then their composition `g ∘ f : α → γ` is antitone.
|
StrictAnti.dual_right
theorem StrictAnti.dual_right :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
StrictAnti f → StrictMono (⇑OrderDual.toDual ∘ f)
This theorem, "`StrictAnti.dual_right`", asserts that for any types `α` and `β` with preorders, and any function `f` from `α` to `β` that is strictly anti-monotone (meaning that if `a < b` then `f(b) < f(a)`), the composition of `f` with the identity function `OrderDual.toDual` (which is basically giving us the reverse order) yields a strictly monotone function. In other words, it says that reversing the order of the inputs to a strictly anti-monotone function gives a strictly monotone function.
More concisely: If `f` is a strictly anti-monotone function between preordered types `α` and `β`, then the composition `f ∘ OrderDual.toDual` is a strictly monotone function.
|
monotone_const
theorem monotone_const :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {c : β}, Monotone fun x => c
The theorem `monotone_const` states that for any two types `α` and `β`, where `α` and `β` have preorder relations, and for any constant `c` of type `β`, the function that assigns to each element of `α` the constant `c` is monotone. In other words, if `a ≤ b` for any `a` and `b` in `α`, it always holds that `c ≤ c`.
More concisely: For any preordered types `α` and `β`, and constant `c` in `β`, the function mapping each `α` element to `c` is monotone. (That is, if `a ≤ b` in `α`, then `c ≤ c`.)
|
Antitone.ne_of_lt_of_lt_int
theorem Antitone.ne_of_lt_of_lt_int :
∀ {α : Type u} [inst : Preorder α] {f : ℤ → α},
Antitone f → ∀ (n : ℤ) {x : α}, f (n + 1) < x → x < f n → ∀ (a : ℤ), f a ≠ x
The theorem `Antitone.ne_of_lt_of_lt_int` states that for any preorder `α`, if `f` is an antitone function from integers `ℤ` to `α`, and if an element `x` of `α` is such that it lies strictly between `f(n + 1)` and `f(n)` for some integer `n`, then `x` is not in the range of the function `f`. In other words, there does not exist an integer `a` such that `f(a)` equals `x`.
More concisely: If `f` is an antitone function from integers `ℤ` to a preorder `α`, then there is no integer `a` such that `f(a) = x` for any `x` strictly between `f(n + 1)` and `f(n)` for some integer `n`.
|
Monotone.dual
theorem Monotone.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → Monotone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
The theorem `Monotone.dual` states that for all types `α` and `β` that have a preorder, and any function `f` from `α` to `β`, if `f` is a monotone function then the function obtained by first applying `f`, then applying the identity function to the `OrderDual` of `α`, and finally applying the identity function from the `OrderDual` of `β`, is also a monotone function. In other words, the monotonicity of a function is preserved when the orders of the domain and codomain are reversed.
More concisely: If `f` is a monotone function between preordered types `α` and `β`, then the function `x ≤ y => y ≤ f(OrderDual x)` is also monotone, where `OrderDual` denotes the dual order.
|
monotone_iff_forall_lt
theorem monotone_iff_forall_lt :
∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β},
Monotone f ↔ ∀ ⦃a b : α⦄, a < b → f a ≤ f b
This theorem states that for any two types `α` and `β`, given a partial order on `α` and a preorder on `β`, a function `f` from `α` to `β` is monotone if and only if for all pairs of elements `a` and `b` from `α` such that `a` is strictly less than `b`, the result of applying `f` to `a` is less than or equal to the result of applying `f` to `b`. In mathematical terms, it states that a function `f: α → β` is monotone (i.e., `a ≤ b` implies `f(a) ≤ f(b)` for all `a, b ∈ α`) if and only if for all `a, b ∈ α` such that `a < b`, we have `f(a) ≤ f(b)`.
More concisely: A function between two types is monotone with respect to given partial orders if and only if the image of any strictly smaller element is less than or equal to the image of any strictly larger element.
|
Antitone.reflect_lt
theorem Antitone.reflect_lt :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
Antitone f → ∀ {a b : α}, f a < f b → b < a
The theorem `Antitone.reflect_lt` states that for any types `α` and `β`, where `α` is a linear order and `β` is a preorder, and for any function `f` from `α` to `β` that is antitone (i.e., if `a ≤ b` then `f(b) ≤ f(a)`), then for any `a` and `b` of type `α`, if `f(a) < f(b)`, it implies that `b < a`. In other words, if `f` is an antitone function, it reflects the strict order from its range to its domain.
More concisely: If `f` is an antitone function from a linear order `α` to a preorder `β`, then `f(a) < f(b)` implies `a > b`.
|
Antitone.ne_of_lt_of_lt_nat
theorem Antitone.ne_of_lt_of_lt_nat :
∀ {α : Type u} [inst : Preorder α] {f : ℕ → α},
Antitone f → ∀ (n : ℕ) {x : α}, f (n + 1) < x → x < f n → ∀ (a : ℕ), f a ≠ x
The theorem `Antitone.ne_of_lt_of_lt_nat` states that, given a function `f` from the natural numbers to some ordered set (`Preorder α`) that is antitone (meaning, it reverses the order; if `a ≤ b` then `f b ≤ f a`), if a value `x` of the ordered set lies strictly between `f` applied to `n + 1` and `f` applied to `n`, then `x` is not in the range of `f`. In other words, there is no natural number `a` for which `f a = x`.
More concisely: If `f` is an antitone function from natural numbers to an ordered set, and there exists a `x` in the ordered set strictly between `f (n + 1)` and `f n` for some natural number `n`, then `x` is not in the range of `f`.
|
Antitone.dual_right
theorem Antitone.dual_right :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Antitone f → Monotone (⇑OrderDual.toDual ∘ f)
The theorem `Antitone.dual_right` states that for any types `α` and `β` with preorders, and any function `f` from `α` to `β`, if `f` is antitone (i.e., if `a ≤ b` then `f b ≤ f a`), then the composition of `f` with the `toDual` function from the `OrderDual` of `α` is monotone (i.e., if `a ≤ b` then `f a ≤ f b`). In other words, reversing the direction of an antitone function results in a monotone function.
More concisely: If `f : α → β` is an antitone function between pre ordered types `α` and `β`, then the composition `f ∘ toDual : OrderDual α → OrderDual β` is a monotone function.
|
antitone_iff_forall_lt
theorem antitone_iff_forall_lt :
∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β},
Antitone f ↔ ∀ ⦃a b : α⦄, a < b → f b ≤ f a
The theorem `antitone_iff_forall_lt` establishes an equivalence between two properties of a function `f` that maps elements from an ordered type `α` to another ordered type `β`. The first property is `Antitone`, which means that `f` is an antitone function (i.e., for all `a` and `b` in `α` where `a ≤ b`, `f b ≤ f a`). The second property is that for every pair of distinct elements `a` and `b` in `α` where `a` is strictly less than `b`, the image of `b` under `f` is less than or equal to the image of `a`. In other words, this theorem states that a function is antitone if and only if its value decreases or stays the same whenever its argument increases strictly.
More concisely: A function between ordered types is antitone if and only if for all distinct elements `a` and `b` with `a < b`, we have `f(b) ≤ f(a)`.
|
Subtype.strictMono_coe
theorem Subtype.strictMono_coe : ∀ {α : Type u} [inst : Preorder α] (t : Set α), StrictMono Subtype.val
This theorem states that for any type `α` with a preorder structure, and for any set `t` of elements of type `α`, the function `Subtype.val` is strictly monotone. In other words, if `a` and `b` are two elements in `t` such that `a < b`, then `Subtype.val a < Subtype.val b`. Here, `Subtype.val` is a function that retrieves the underlying element of a subtype. The theorem is saying that retrieving the underlying elements preserves the strict order.
More concisely: For any preorder type `α` and subset `t` of `α`, the function `Subtype.val` maps strictly smaller elements to strictly smaller values, that is, if `a` is strictly smaller than `b` in `t`, then `Subtype.val(a)` is strictly smaller than `Subtype.val(b)`.
|
Int.exists_strictAnti
theorem Int.exists_strictAnti :
∀ (α : Type u) [inst : Preorder α] [inst_1 : Nonempty α] [inst_2 : NoMinOrder α] [inst_3 : NoMaxOrder α],
∃ f, StrictAnti f
This theorem states that if we have a nonempty set `α` that is ordered (preorder), but it does not contain any minimal or maximal elements, then there exists a function `f` that maps integers (`ℤ`) to elements of `α` in a strictly antitone manner. In other words, if for two integers `a` and `b` we have `a < b`, then `f(b) < f(a)`. This function `f` is decreasing when going from `a` to `b`.
More concisely: If `α` is a nonempty, preordered set without minimal or maximal elements, then there exists a strictly antitone function `f : ℤ → α`.
|
Antitone.comp
theorem Antitone.comp :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
{f : α → β}, Antitone g → Antitone f → Monotone (g ∘ f)
This theorem states that if we have two types `α`, `β`, and `γ` which have the `Preorder` property (i.e., they support operations of comparison like less than or equal to), then for any two functions `f : α → β` and `g : β → γ`, if `f` is antitone (meaning that for any two elements in `α`, if the first is less than or equal to the second, then the result of applying `f` to the second is less than or equal to the result of applying `f` to the first) and `g` is also antitone, then the composition of `g` and `f` (i.e., `g ∘ f`) is monotone (meaning that for any two elements in `α`, if the first is less than or equal to the second, then the result of applying `g ∘ f` to the first is less than or equal to the result of applying `g ∘ f` to the second).
More concisely: If `α`, `β`, and `γ` are preordered types, and `f : α → β` and `g : β → γ` are antitone functions, then `g ∘ f` is a monotone function.
|
StrictMono.dual
theorem StrictMono.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
StrictMono f → StrictMono (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
The theorem `StrictMono.dual` states that for any two types `α` and `β` with preorder relations, and any function `f` from `α` to `β`, if `f` is strictly monotone, then the function formed by first applying the function `f`, then applying the `OrderDual.toDual` function, and then applying the `OrderDual.ofDual` function is also strictly monotone. In other words, a strictly monotone function remains strictly monotone even when the order of its inputs is reversed.
More concisely: If `f` is a strictly monotone function between preordered types `α` and `β`, then the composition of `f`, `OrderDual.toDual`, and `OrderDual.ofDual` is also a strictly monotone function.
|
Antitone.dual_left
theorem Antitone.dual_left :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Antitone f → Monotone (f ∘ ⇑OrderDual.ofDual)
The theorem `Antitone.dual_left` states that for any types `α` and `β`, both equipped with a preorder relation, and for any function `f` from `α` to `β`, if `f` is antitone (meaning, if `a ≤ b` then `f b ≤ f a`), then the composition of `f` with the identity function on the dual order of `α` is monotone (meaning, if `a ≤ b` in the dual order then `f a ≤ f b` in `β`). In essence, this theorem asserts that an antitone function becomes a monotone function when applied to the dual of an ordered type.
More concisely: If `f: α → β` is antitone between preordered types `α` and `β`, then `f ∘ Id_α'` is monotone, where `Id_α'` is the identity function on the dual order of `α`.
|
Int.exists_strictMono
theorem Int.exists_strictMono :
∀ (α : Type u) [inst : Preorder α] [inst_1 : Nonempty α] [inst_2 : NoMinOrder α] [inst_3 : NoMaxOrder α],
∃ f, StrictMono f
The theorem `Int.exists_strictMono` states that given a type `α` with a preorder structure, which is not empty and has neither minimal nor maximal elements, there exists a function `f` from the integers (`ℤ`) to `α` that is strictly monotone. This means that for any two distinct integers, the value of `f` at the larger integer is strictly greater than the value of `f` at the smaller one.
More concisely: Given a preorder structure on a non-empty type without minimal or maximal elements, there exists a strictly monotone function from the integers to that type.
|
monotone_fst
theorem monotone_fst : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β], Monotone Prod.fst := by
sorry
The theorem `monotone_fst` states that for any types `α` and `β` with preorders defined on them, the `Prod.fst` function is monotone. This means that if we have a pair of elements from `α × β` where the first element of the first pair is less than or equal to the first element of the second pair, then the result of applying `Prod.fst` (which essentially projects out the first component of the pair) on the first pair will be less than or equal to the result of applying `Prod.fst` on the second pair.
More concisely: For all preordered types `α` and `β`, the `Prod.fst` function on `α × β` is monotone, i.e., `Prod.fst (x, y) ≤ Prod.fst (x', y')` whenever `x ≤ x'`.
|
StrictAnti.strictAntiOn
theorem StrictAnti.strictAntiOn :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
StrictAnti f → ∀ (s : Set α), StrictAntiOn f s
The theorem `StrictAnti.strictAntiOn` states that for all types `α` and `β` (with pre-defined preorders) and for all function `f` from `α` to `β`, if the function `f` is strictly antitone (meaning that if `a` is less than `b`, then `f(b)` is less than `f(a)`), then for any set `s` of type `α`, the function `f` is also strictly antitone on the set `s`. In other words, for any elements `a` and `b` in the set `s`, if `a` is less than `b`, then `f(b)` is less than `f(a)`.
More concisely: If `f` is a strictly antitone function from type `α` to type `β` with pre-defined preorders, then `f` is strictly antitone on any set `s` of type `α`.
|
MonotoneOn.dual_left
theorem MonotoneOn.dual_left :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
MonotoneOn f s → AntitoneOn (f ∘ ⇑OrderDual.ofDual) s
This theorem, `MonotoneOn.dual_left`, states that for any given types `α` and `β` with preorder relations, and any function `f` from `α` to `β` and any set `s` of type `α`, if the function `f` is monotone on the set `s`, then the function obtained by composing `f` with the identity function on the dual order of `α` is antitone on the set `s`. In simpler terms, it states that a monotone function becomes an antitone function when the order is reversed.
More concisely: If `f` is a monotonic function from type `α` to type `β` and `s` is a subset of `α`, then the composite function `f ∘ id` (where `id` is the identity function on the dual order of `α`) is an antitone function on `s`.
|
StrictMono.comp_strictAnti
theorem StrictMono.comp_strictAnti :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
{f : α → β}, StrictMono g → StrictAnti f → StrictAnti (g ∘ f)
The theorem `StrictMono.comp_strictAnti` states that for all types `α`, `β`, and `γ` with preorders and given any two functions `g: β → γ` and `f: α → β`, if `g` is strictly monotone and `f` is strictly antitone, then the composition of `g` with `f` (denoted by `g ∘ f`) is strictly antitone. In other words, if `g` preserves the order strictly and `f` reverses the order strictly, their composition also reverses the order strictly.
More concisely: If functions `f: α → β` is strictly antitone and `g: β → γ` is strictly monotone, then their composition `g ∘ f: α → γ` is strictly antitone.
|
Nat.exists_strictAnti'
theorem Nat.exists_strictAnti' :
∀ {α : Type u} [inst : Preorder α] [inst_1 : NoMinOrder α] (a : α), ∃ f, StrictAnti f ∧ f 0 = a
The theorem states that for any type `α` that has a preorder structure and does not have any minimal elements, given any element `a` of `α`, there exists a function `f` from natural numbers to `α` that is strictly antitone (meaning the function decreases at every step, i.e., if `n` is less than `m`, then `f(m)` is less than `f(n)`) and has `f(0)` equal to the given element `a`. In other words, we can always find a strictly decreasing sequence in `α` that starts at any given point.
More concisely: For any preorder type `α` without minimal elements, given any `a` in `α`, there exists a strictly antitone function `f : ℕ → α` with `f(0) = a`.
|
Monotone.strictMono_of_injective
theorem Monotone.strictMono_of_injective :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : PartialOrder β] {f : α → β},
Monotone f → Function.Injective f → StrictMono f
This theorem states that for any types `α` and `β` with preorder `α` and partial order `β`, and any function `f` from `α` to `β`, if `f` is both monotone and injective, then `f` is strictly monotone.
In other words, if a function `f` satisfies two properties - first, being monotone, meaning that if an element `a` of type `α` is less than or equal to another element `b` of `α`, then `f(a)` is less than or equal to `f(b)`; and second, being injective, meaning that if `f(a)` equals `f(b)`, then `a` must equal `b` - then `f` is strictly monotone, which means that if `a < b`, then `f(a) < f(b)`.
More concisely: If `f` is a function from a preordered type `α` to a partially ordered type `β` that is both monotone and injective, then it is strictly monotone.
|
not_monotone_not_antitone_iff_exists_le_le
theorem not_monotone_not_antitone_iff_exists_le_le :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
This theorem states that for any function `f` mapping from one linearly ordered type `α` to another `β`, the function is neither strictly increasing (monotone) nor strictly decreasing (antitone) if and only if there exist elements `a`, `b`, and `c` in `α` such that `a` ≤ `b` ≤ `c` and either `f(a)` < `f(b)` and `f(c)` < `f(b)` (forming an upright "dent" in the function) or `f(b)` < `f(a)` and `f(b)` < `f(c)` (forming a downward "dent" in the function).
More concisely: A function `f` from a linearly ordered type `α` to another `β` is neither strictly increasing nor strictly decreasing if and only if there exist `a ≤ b ≤ c` in `α` such that `f(a) < f(b) < f(c)` or `f(b) < f(a) < f(c)`.
|
StrictMono.cmp_map_eq
theorem StrictMono.cmp_map_eq :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
StrictMono f → ∀ (x y : α), cmp (f x) (f y) = cmp x y
The theorem `StrictMono.cmp_map_eq` asserts that for any two values `x` and `y` of a type `α`, given that we have a linear ordering defined on `α` and `β` and a strictly monotonic function `f` mapping from `α` to `β`, the comparison of `f(x)` and `f(y)` using the function `cmp` will yield the same result as the comparison of `x` and `y`. In other words, the ordering of `x` and `y` is preserved under the strictly monotonic function `f`.
More concisely: For any strictly monotonic function `f` between linearly ordered types `α` and `β`, and all `x y` in `α`, we have `x ≤ y` if and only if `f(x) ≤ f(y)`.
|
MonotoneOn.dual
theorem MonotoneOn.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
MonotoneOn f s → MonotoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
The theorem `MonotoneOn.dual` states that for any set `s` of some type `α` and any function `f` from `α` to some type `β`, if `f` is monotone on `s` (meaning that for all `a, b` in `s`, if `a ≤ b`, then `f(a) ≤ f(b)`), then the function composed of applying `f` to the dual order of `α` (i.e., applying the function `OrderDual.toDual` after `f` and then applying `OrderDual.ofDual`) is also monotone on `s`. The dual order is simply the original order reversed.
More concisely: If `f` is a monotone function from a set `s` to type `β`, then the composition of `f` with the dual order on `α` is also a monotone function on `s`.
|
strictMono_nat_of_lt_succ
theorem strictMono_nat_of_lt_succ :
∀ {α : Type u} [inst : Preorder α] {f : ℕ → α}, (∀ (n : ℕ), f n < f (n + 1)) → StrictMono f
The theorem `strictMono_nat_of_lt_succ` states that for any type `α` with a preorder structure and any function `f` from natural numbers to `α`, if for every natural number `n`, the value `f(n)` is less than the value `f(n + 1)`, then the function `f` is strictly monotone. In mathematical terms, if $f(n) < f(n + 1)$ for all natural numbers $n$, then $a < b$ implies $f(a) < f(b)$ for all natural numbers $a$ and $b$.
More concisely: If `f` is a function from natural numbers to a type with a preorder structure and `f(n)` is less than `f(n+1)` for all natural numbers `n`, then `f` is strictly monotone, that is, `a < b` implies `f(a) < f(b)` for all natural numbers `a` and `b`.
|
StrictMonoOn.eq_iff_eq
theorem StrictMonoOn.eq_iff_eq :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictMonoOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → (f a = f b ↔ a = b)
The theorem `StrictMonoOn.eq_iff_eq` states that for any types `α` and `β` where `α` is a linear order and `β` is a preorder, for any function `f` from `α` to `β`, and for any set `s` of elements of type `α`, if the function `f` is strictly monotone on the set `s`, then for all `a` and `b` in `s`, `f(a)` equals `f(b)` if and only if `a` equals `b`. In other words, a strictly monotone function on a set does not map different elements in the set to the same value.
More concisely: A strictly monotone function from a linear order to a preorder maps distinct elements to distinct images.
|
StrictMonoOn.dual_left
theorem StrictMonoOn.dual_left :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictMonoOn f s → StrictAntiOn (f ∘ ⇑OrderDual.ofDual) s
This theorem, `StrictMonoOn.dual_left`, states that for any two types `α` and `β`, both endowed with a preorder relation, and any function `f` from `α` to `β`, if `f` is strictly monotone on a set `s` of `α`, then the composition of `f` with the function `OrderDual.ofDual` (which is the identity function on the order reverse of `α`) is strictly antitone on the same set `s`. In other words, if `f` strictly increases over `s`, then `f` composed with the order reversing function strictly decreases over `s`.
More concisely: If `f: α → β` is strictly monotone on `s subseteq α` and `OrderDual.ofDual` is the order reversing function on `α`, then `f ∘ OrderDual.ofDual` is strictly antitone on `s`.
|
Antitone.antitoneOn
theorem Antitone.antitoneOn :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Antitone f → ∀ (s : Set α), AntitoneOn f s
This theorem states that for any two types `α` and `β` with preordered structures and a function `f` from `α` to `β`, if `f` is antitone (i.e., for all `a` and `b` in `α`, if `a` is less than or equal to `b` then `f(b)` is less than or equal to `f(a)`), then `f` is also antitone on any set `s` of type `α`. In other words, for any `a` and `b` in set `s`, if `a` is less than or equal to `b`, then `f(b)` is less than or equal to `f(a)`.
More concisely: If `f` is an antitone function from preordered types `α` to `β`, then `f` is antitone on any subset `s` of `α`.
|
StrictAntiOn.dual_left
theorem StrictAntiOn.dual_left :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictAntiOn f s → StrictMonoOn (f ∘ ⇑OrderDual.ofDual) s
This theorem states that for any set `s` of elements of a certain type `α`, and a function `f` mapping `α` to `β`, if `f` is strictly antitone on `s` (meaning, for all `a, b` in `s`, if `a < b`, then `f(b) < f(a)`), then the composition of `f` and the identity function on the dual order of `α` is strictly monotone on `s` (i.e., for all `a, b` in `s`, if `a < b`, then `f(a) < f(b)` after applying the identity function). Essentially, it translates the property of being strictly decreasing into being strictly increasing under a change of order.
More concisely: If `f` is a strictly antitone function from a set `α` to `β`, then the composition of `f` and the identity function on the dual order of `α` is a strictly increasing function on `α`.
|
StrictMono.le_iff_le
theorem StrictMono.le_iff_le :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
StrictMono f → ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
This theorem states that for all types `α` and `β`, if `α` is a linearly ordered type and `β` is a preordered type, and if we have a function `f` from `α` to `β` that is strictly monotone, then for all elements `a` and `b` of `α`, the function `f` applied to `a` is less than or equal to `f` applied to `b` if and only if `a` is less than or equal to `b`. In other words, a strictly monotone function preserves the order relation from its domain to its codomain.
More concisely: A strictly monotone function from a linearly ordered type to a preordered type preserves the order relation.
|
StrictMonoOn.le_iff_le
theorem StrictMonoOn.le_iff_le :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictMonoOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → (f a ≤ f b ↔ a ≤ b)
The theorem `StrictMonoOn.le_iff_le` states that for any set `s` of elements of a certain type `α`, and for any function `f` from `α` to another type `β`, given that the types `α` and `β` have a linear and a preorder relationship respectively, if the function `f` is strictly monotone on the set `s`, then for any two elements `a` and `b` in the set `s`, `f(a)` is less than or equal to `f(b)` if and only if `a` is less than or equal to `b`. In other words, the ordering of `a` and `b` in `α` is preserved under `f` in `β`.
More concisely: If `f` is a strictly monotone function from a set `s` of type `α` to a preordered type `β`, then for all `a, b ∈ s`, `a ≤ b` implies `f(a) ≤ f(b)`.
|
Antitone.dual
theorem Antitone.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Antitone f → Antitone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
The theorem `Antitone.dual` states that for any types `α` and `β` that are both preordered, and for any function `f` from `α` to `β` that is antitone (i.e., the function is decreasing in the sense that if `a` is less than or equal to `b` then `f(b)` is less than or equal to `f(a)`), the function obtained by first applying the function `f`, then applying the identity function `toDual` on the order dual of `α`, and finally applying the identity function `ofDual` on the order dual of `β`, is also antitone. In other words, if a function is decreasing in a certain order, it remains decreasing even if we consider the dual order.
More concisely: If `f: α → β` is an antitone function between preordered types `α` and `β`, then the function `ofDual ∘ f ∘ toDual: β^dual → α^dual` is also antitone.
|
monotone_snd
theorem monotone_snd : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β], Monotone Prod.snd := by
sorry
This theorem, `monotone_snd`, states that for any types `α` and `β` that are both ordered (preorder), the function `Prod.snd`, which returns the second element of a pair, is a monotone function. This means that if we have a pair `(a, b)` and `(c, d)`, where `a ≤ c`, then `b ≤ d`. Thus, the order of the second elements in the pairs is preserved.
More concisely: For any preordered types `α` and `β`, the second projection `Prod.snd` on pairs of type `(α × β)` is a monotone function, preserveing the order of the second components.
|
antitone_nat_of_succ_le
theorem antitone_nat_of_succ_le :
∀ {α : Type u} [inst : Preorder α] {f : ℕ → α}, (∀ (n : ℕ), f (n + 1) ≤ f n) → Antitone f
The theorem `antitone_nat_of_succ_le` states that for any type `α` that has a preorder, and any function `f` from natural numbers to `α`, if for all natural number `n`, `f(n + 1)` is less than or equal to `f(n)`, then the function `f` is antitone. In other words, if a function `f` decreases or remains the same at each step when moving from `n` to `n+1`, then `f` is defined as antitone, meaning that it preserves the order when the order of arguments is reversed.
More concisely: If a function from natural numbers to a preordered type decreases or is constant at each successor step, then it is antitone.
|
StrictMono.dual_left
theorem StrictMono.dual_left :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
StrictMono f → StrictAnti (f ∘ ⇑OrderDual.ofDual)
This theorem, `StrictMono.dual_left`, states that for any types `α` and `β` with preorder relations (a reflexive and transitive binary relation), and any function `f` from `α` to `β`, if `f` is strictly monotone (meaning that `f` preserves the order relation in the sense that if `a < b` then `f(a) < f(b)`), then `f` composed with the identity function on the order dual of `α` (which essentially reverses the order relation on `α`) is strictly anti-monotone (meaning that if `a < b` then `f(b) < f(a)`). In other words, if a function is strictly increasing in the original order, it becomes strictly decreasing when the order is reversed.
More concisely: If `f` is a strictly monotone function from `α` to `β` with respect to a preorder relation, then `f` composed with the identity function on the order dual of `α` is strictly anti-monotone.
|
StrictMonoOn.compares
theorem StrictMonoOn.compares :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictMonoOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → ∀ {o : Ordering}, o.Compares (f a) (f b) ↔ o.Compares a b
The theorem `StrictMonoOn.compares` states that for a given type `α` with a linear order structure, type `β` with a preorder structure, a function `f` from `α` to `β`, and a set `s` of elements in `α`, if the function `f` is strictly monotone on the set `s`, then for any two elements `a` and `b` in set `s` and for any ordering `o`, the ordering relationship `o` between `f(a)` and `f(b)` corresponds exactly to the same ordering relationship `o` between `a` and `b`. This implies that a strictly monotone function preserves the order of elements in the set upon which it's monotone.
More concisely: If `f: α → β` is a strictly monotone function on a linearly ordered set `s ⊆ α`, then for all `a, b ∈ s`, `a o b` if and only if `f(a) o f(b)`, where `o` is any ordering on `α`.
|
StrictMono.lt_iff_lt
theorem StrictMono.lt_iff_lt :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
StrictMono f → ∀ {a b : α}, f a < f b ↔ a < b
This theorem states that for all types `α` and `β`, where `α` has a linear order and `β` has a preorder, and for any strictly monotone function `f` from `α` to `β`, then for all `a` and `b` of type `α`, `f(a)` is less than `f(b)` if and only if `a` is less than `b`. In other words, in the context of the given types and orders, a function is strictly monotone if and only if the order of its inputs is preserved when they are mapped under the function.
More concisely: For any strictly monotone function between a linearly ordered type and a preordered type, input order preservation holds: if $a < b$ in the domain, then $f(a) < f(b)$ in the codomain.
|
monotone_toDual_comp_iff
theorem monotone_toDual_comp_iff :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone (⇑OrderDual.toDual ∘ f) ↔ Antitone f
This theorem states that for any two types `α` and `β` with preorder relations, and any function `f` from `α` to `β`, the function `f` is monotonic (meaning, if `a` is less than or equal to `b`, then `f(a)` is less than or equal to `f(b)`) under the dual order if and only if `f` is antitone (meaning, if `a` is less than or equal to `b`, then `f(b)` is less than or equal to `f(a)`) under the original order. In other words, applying the dual order to a monotonic function makes it an antitone function, and vice versa.
More concisely: For any function between two types with preorder relations, it is monotonic under the dual order if and only if it is antitone under the original order.
|
StrictAntiOn.dual_right
theorem StrictAntiOn.dual_right :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictAntiOn f s → StrictMonoOn (⇑OrderDual.toDual ∘ f) s
The theorem `StrictAntiOn.dual_right` states that, for any given set `s` of type `α`, and a function `f` from `α` to `β`, if `f` is strictly antitone on `s` (meaning that for any two elements `a` and `b` in `s`, `a < b` implies `f(b) < f(a)`), then the composition of `f` and the identity function on the dual ordered set `OrderDual.toDual` is strictly monotone on `s` (i.e., for any two elements `a` and `b` in `s`, `a < b` implies that the result of applying `f` to `a` and 'dualizing' is less than the result of applying `f` to `b` and 'dualizing'). In other words, if `f` reverses order in `s`, then when applied to the dual order, `f` preserves the order in `s`.
More concisely: If `f` is a strictly antitone function from a set `α` to `β`, then the composition of `f` and the identity function on the dual order of `α` is a strictly monotone function on `α`.
|
StrictMonoOn.dual_right
theorem StrictMonoOn.dual_right :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictMonoOn f s → StrictAntiOn (⇑OrderDual.toDual ∘ f) s
The theorem `StrictMonoOn.dual_right` states that for any types `α` and `β` with preorder structures, any function `f` from `α` to `β`, and any set `s` of type `α`, if `f` is strictly monotone on `s` (that is, for all `a, b` in `s`, `a < b` implies `f(a) < f(b)`), then the composition of `f` with the `OrderDual.toDual` function is strictly antitone on `s` (that is, for all `a, b` in `s`, `a < b` implies `f(b) < f(a)`). Essentially, the theorem highlights a correspondence between strictly increasing functions and strictly decreasing functions when we consider the dual ordering.
More concisely: If `f : α → β` is a strictly monotone function on a preordered set `s : set α`, then the composition `OrderDual.toDual ∘ f` is strictly antitone on `s`.
|
StrictMono.comp
theorem StrictMono.comp :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
{f : α → β}, StrictMono g → StrictMono f → StrictMono (g ∘ f)
The theorem `StrictMono.comp` states that for all types `α`, `β`, and `γ` with preorder relations, if a function `g` from `β` to `γ` and a function `f` from `α` to `β` are both strictly monotone (that is, for any two elements `a` and `b` such that `a < b`, `f a < f b` and `g a < g b`), then the composition of `g` and `f` (denoted by `g ∘ f`) is also strictly monotone. In other words, the property of being strictly monotone is preserved under function composition.
More concisely: If functions `f: α → β` and `g: β → γ` are strictly monotone, then their composition `g ∘ f: α → γ` is also strictly monotone.
|
StrictMonoOn.dual
theorem StrictMonoOn.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictMonoOn f s → StrictMonoOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
This theorem states that for all types `α` and `β` with preorders, a function `f` from `α` to `β`, and a set `s` of type `α`, if the function `f` is strictly monotone on the set `s`, then the function obtained by composing `f` with the identity functions `OrderDual.toDual` and `OrderDual.ofDual` (essentially a function equivalent to `f` but on the dual order) is also strictly monotone on the set `s`. In simpler terms, if a function is strictly increasing on a set, then the same function is also strictly increasing on the set when considering elements in reverse order.
More concisely: If `f` is a strictly monotone function from type `α` to type `β` with preorders, then the function `OrderDual.ofDual ∘ f ∘ OrderDual.toDual` is also strictly monotone on any set `s` in `α`.
|
StrictAntiOn.dual
theorem StrictAntiOn.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictAntiOn f s → StrictAntiOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
The theorem `StrictAntiOn.dual` states that for any given types `α` and `β` with preorder structures (meaning, they are partially ordered and allow comparison of elements), if a function `f` from `α` to `β` is strictly anti-monotone on a set `s` of `α` (i.e., `f` decreases on increasing inputs within `s`), then the function `f` composed with the dual order on `α` remains strictly anti-monotone on `s`. In other words, the ordering of `α` can be reversed without affecting the strict anti-monotonicity property of `f` on `s`.
More concisely: If `f` is strictly anti-monotone on a set `s` of a partially ordered type `α`, then `f` composed with the dual order on `α` remains strictly anti-monotone on `s`.
|
Nat.exists_strictAnti
theorem Nat.exists_strictAnti :
∀ (α : Type u) [inst : Preorder α] [inst_1 : Nonempty α] [inst_2 : NoMinOrder α], ∃ f, StrictAnti f
This theorem states that if `α` is a nonempty preorder (an ordered set where every two elements are comparable) that does not have any minimal elements, then there exists a function `f` from the set of natural numbers `ℕ` to `α` that is strictly antitone. A function is strictly antitone if for any two natural numbers `a` and `b`, `a < b` implies `f(b) < f(a)`. In other words, as the input increases, the output strictly decreases.
More concisely: If `α` is a nonempty preorder without minimal elements, there exists a strictly antitone function `f : ℕ → α`.
|
Subtype.mono_coe
theorem Subtype.mono_coe : ∀ {α : Type u} [inst : Preorder α] (t : Set α), Monotone Subtype.val
The theorem `Subtype.mono_coe` states that for any type `α` that has a preorder structure and any set `t` of `α`, the function `Subtype.val` is monotone. In other words, if we have two elements of a subtype such that one is less than or equal to the other, then their underlying elements in the base type `α`, obtained using `Subtype.val`, also uphold this order.
More concisely: For any preordered type `α` and subtype `t ⊆ α`, the function `Subtype.val` preserves the ordering, i.e., `x ≤ y` in `t` implies `Subtype.val x ≤ Subtype.val y` in `α`.
|
Monotone.iterate
theorem Monotone.iterate : ∀ {α : Type u} [inst : Preorder α] {f : α → α}, Monotone f → ∀ (n : ℕ), Monotone f^[n] := by
sorry
The theorem `Monotone.iterate` states that for any type `α` with a preorder, and any monotone function `f : α → α`, the `n`-th iterate of `f`, denoted by `f^[n]`, is also a monotone function. Here, the `n`-th iterate of `f` is the function obtained by composing `f` with itself `n` times, i.e., applying `f` `n` times successively. In other words, if `f` preserves the order of elements, so does any number of successive applications of `f`.
More concisely: For any type `α` with a preorder and any monotone function `f : α → α`, the `n`-th iterate `f^[n]` is also a monotone function.
|
Monotone.ne_of_lt_of_lt_nat
theorem Monotone.ne_of_lt_of_lt_nat :
∀ {α : Type u} [inst : Preorder α] {f : ℕ → α},
Monotone f → ∀ (n : ℕ) {x : α}, f n < x → x < f (n + 1) → ∀ (a : ℕ), f a ≠ x
The theorem `Monotone.ne_of_lt_of_lt_nat` states that for any preorder `α`, given a monotone function `f` from the set of natural numbers `ℕ` to `α`, if there exists a natural number `n` such that an element `x` from `α` lies strictly between `f(n)` and `f(n + 1)`, then `x` is not in the range of the function `f`. In other words, no natural number `a` can be found such that `f(a) = x`.
More concisely: If a monotonic function from natural numbers to a preorder has an element strictly between its images of two consecutive natural numbers, then that element is not in the function's range.
|
Monotone.dual_right
theorem Monotone.dual_right :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → Antitone (⇑OrderDual.toDual ∘ f)
The theorem `Monotone.dual_right` states that for any types `α` and `β` equipped with preorder structures, and for any function `f` from `α` to `β`, if the function `f` is monotone (i.e., if for any `a` and `b` in `α`, `a ≤ b` implies `f(a) ≤ f(b)`), then the function formed by composing `f` with the `toDual` function of the `OrderDual` of `α` (which effectively reverses the order) is antitone. This means that for any `a` and `b` in `α`, `a ≤ b` implies that `f(b)` is less than or equal to `f(a)` when considering the reversed order. In other words, if `f` preserves the order of elements, then the dual function reverses the order.
More concisely: If `f` is a monotone function from a preordered type `α` to a preordered type `β`, then the composition of `f` and the order dual function `toDual` is an antitone function.
|
Function.monotone_eval
theorem Function.monotone_eval :
∀ {ι : Type u} {α : ι → Type v} [inst : (i : ι) → Preorder (α i)] (i : ι), Monotone (Function.eval i)
The theorem `Function.monotone_eval` states that for any type `ι`, any function `α` from `ι` to some type, and for any index `i` in `ι`, if each type `α i` has a preorder (i.e., an order relation that is reflexive and transitive), then the evaluation function at `i` is monotone. In other words, if `a` and `b` are elements of type `α i` and `a` is less than or equal to `b`, then the value of any function evaluated at `a` is less than or equal to the value of the function evaluated at `b`. This theorem asserts the consistency of order when applying functions under certain conditions.
More concisely: If `α : Type ι → Type*, i : ι, and `α i carries a preorder, then the evaluation function `Function.eval : α i → α (succ i) → Prop` is monotone.
|
Int.rel_of_forall_rel_succ_of_lt
theorem Int.rel_of_forall_rel_succ_of_lt :
∀ {β : Type v} (r : β → β → Prop) [inst : IsTrans β r] {f : ℤ → β},
(∀ (n : ℤ), r (f n) (f (n + 1))) → ∀ ⦃a b : ℤ⦄, a < b → r (f a) (f b)
This theorem, `Int.rel_of_forall_rel_succ_of_lt`, states that for any type `β` and a binary relation `r` on `β` that is transitive, and a function `f` mapping from integers to `β`, if for all integers `n`, `f(n)` is related to `f(n+1)` by `r`, then for any two integers `a` and `b` with `a < b`, `f(a)` is related to `f(b)` by `r`. Essentially, this says that if each integer is related to its successor via `f` and `r`, then any two integers in increasing order are related in the same way through `f` and `r`.
More concisely: If `r` is a transitive relation on type `β` and for all integers `n`, `f(n)` is related to `f(n+1)` by `r`, then for any integers `a` and `b` with `a < b`, `f(a)` is related to `f(b)` by `r`.
|
monotone_nat_of_le_succ
theorem monotone_nat_of_le_succ :
∀ {α : Type u} [inst : Preorder α] {f : ℕ → α}, (∀ (n : ℕ), f n ≤ f (n + 1)) → Monotone f
The theorem `monotone_nat_of_le_succ` states that for any type `α` that satisfies the `Preorder` condition (meaning it has defined operations for comparison and ordering), and a function `f` from natural numbers to `α`, if for every natural number `n`, the function `f` applied to `n` is less than or equal to `f` applied to `n + 1`, then the function `f` is monotone. In mathematical terms, this theorem asserts that a function `f : ℕ -> α` is monotone if `f(n) ≤ f(n+1)` for all `n` in natural numbers.
More concisely: A function `f : ℕ -> α` is monotone if `f(n) ≤ f(n+1)` for all natural numbers `n`.
|
StrictMono.injective
theorem StrictMono.injective :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
StrictMono f → Function.Injective f
The theorem `StrictMono.injective` states that for all types `α` and `β`, where `α` has a linear order structure and `β` has a preorder structure, any function `f` from `α` to `β` that is strictly monotone is also injective. In other words, if a function `f` strictly increases or decreases (as dictated by strict monotonicity) for all elements in `α`, then it will never map distinct elements in `α` to the same element in `β`, which is the definition of injectivity.
More concisely: A strictly monotone function between linearly ordered and preordered types is injective.
|
strictMono_of_le_iff_le
theorem strictMono_of_le_iff_le :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
(∀ (x y : α), x ≤ y ↔ f x ≤ f y) → StrictMono f
The theorem `strictMono_of_le_iff_le` states that for any types `α` and `β` with preorder relations, and any function `f` from `α` to `β`, if for all `x` and `y` in `α`, `x` is less than or equal to `y` if and only if `f(x)` is less than or equal to `f(y)`, then the function `f` is strictly monotone. In other words, this theorem establishes that a function preserving the order of elements implies that the function is strictly increasing.
More concisely: If a function between preordered types preserves the order relation, then it is strictly increasing.
|
MonotoneOn.dual_right
theorem MonotoneOn.dual_right :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
MonotoneOn f s → AntitoneOn (⇑OrderDual.toDual ∘ f) s
The theorem `MonotoneOn.dual_right` states that given any types `α` and `β` that have a preorder relation, along with a function `f : α → β` and a set `s` of type `α`, if the function `f` is monotone on the set `s`, then the function `f` composed with the identity function to the dual order (i.e., `⇑OrderDual.toDual ∘ f`) is antitone on the same set `s`. In other words, if a function preserves the order of elements in a set, then flipping the order of the elements also flips the direction of the function, making it antitone.
More concisely: If `f : α → β` is a monotone function on set `s ⊆ α`, then the composition `OrderDual.toDual �circ f` is an antitone function on `s`.
|
StrictMonoOn.monotoneOn
theorem StrictMonoOn.monotoneOn :
∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictMonoOn f s → MonotoneOn f s
The theorem `StrictMonoOn.monotoneOn` states that for any set `s` of a certain type `α`, and a function `f` from `α` to another type `β`, if `f` is strictly monotone on `s` then `f` is also monotone on `s`. Here, a function is said to be strictly monotone on `s` if for any two elements `a` and `b` in `s`, `a < b` implies `f(a) < f(b)`, and it is said to be monotone on `s` if `a ≤ b` implies `f(a) ≤ f(b)`. This theorem illustrates a property of monotonicity: strict monotonicity implies general monotonicity.
More concisely: If a function is strictly monotonic on a set, then it is monotonic on that set.
|
Antitone.comp_monotone
theorem Antitone.comp_monotone :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
{f : α → β}, Antitone g → Monotone f → Antitone (g ∘ f)
This theorem states that for any three types `α`, `β`, and `γ` with preorders, if `g` is a function from `β` to `γ` that is antitone (meaning that if `a ≤ b` then `g(b) ≤ g(a)`) and `f` is a function from `α` to `β` that is monotone (meaning that if `a ≤ b` then `f(a) ≤ f(b)`), then the composition of `g` and `f` (effectively `g(f(x))`) is also an antitone function. In other words, composing an antitone function with a monotone function results in an antitone function.
More concisely: If `f` is a monotone function from `α` to `β` and `g` is an antitone function from `β` to `γ`, then the composition `g ∘ f` is an antitone function from `α` to `γ`.
|
StrictAnti.le_iff_le
theorem StrictAnti.le_iff_le :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
StrictAnti f → ∀ {a b : α}, f a ≤ f b ↔ b ≤ a
The theorem, `StrictAnti.le_iff_le`, states that for any types `α` and `β`, which have the structure of a linear order and a preorder respectively, and for any function `f` from `α` to `β` that is strictly antitone (meaning if `a < b` then `f(b) < f(a)`), the statement `f(a) ≤ f(b)` is equivalent to `b ≤ a`. This simply expresses that if we have a strictly decreasing function between two ordered sets, then the order of the function values reverses the order of their arguments.
More concisely: For any strictly antitone function between linearly ordered types, the order of their images reverses the order of their arguments.
|
strictMono_comp_ofDual_iff
theorem strictMono_comp_ofDual_iff :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
StrictMono (f ∘ ⇑OrderDual.ofDual) ↔ StrictAnti f
This theorem states that for any two types `α` and `β` that are preordered, and for any function `f` from `α` to `β`, the function `f` composed with the identity function `OrderDual.ofDual` is strictly monotone if and only if `f` itself is strictly antitone. In other words, a strictly increasing transformation of the dual order implies that the original function is strictly decreasing. The dual order is simply the original order with the direction of the inequalities reversed.
More concisely: For any preordered types `α` and `β` and function `f` from `α` to `β`, `f` is strictly antitone if and only if `f ∘ OrderDual.ofDual` is strictly monotone.
|
Monotone.monotoneOn
theorem Monotone.monotoneOn :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → ∀ (s : Set α), MonotoneOn f s
The theorem `Monotone.monotoneOn` states that for any types `α` and `β` that have a preorder relation, and for any function `f` from `α` to `β`, if `f` is monotone (i.e., for all `a, b` in `α`, if `a ≤ b` then `f(a) ≤ f(b)`), then `f` is also monotone on any set `s` of elements of `α`. In other words, for all `a, b` in `s`, if `a ≤ b` then `f(a) ≤ f(b)`. That is, the global property of monotonicity for a function implies its local property of monotonicity on any subset of its domain.
More concisely: If `f` is a monotone function between preordered types `α` and `β`, then `f` is monotone on any subset `s` of `α`.
|
StrictMono.strictMonoOn
theorem StrictMono.strictMonoOn :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
StrictMono f → ∀ (s : Set α), StrictMonoOn f s
This theorem states that for any types `α` and `β` that have a preorder, and for any function `f` from `α` to `β`, if `f` is strictly monotonic, then `f` is strictly monotonic on any given set `s` of type `α`. In mathematical terms, this means that if for all `a` and `b` in `α` such that `a < b`, we have `f(a) < f(b)`, then for any subset `s` of `α`, if `a` and `b` are in `s` and `a < b`, we also have `f(a) < f(b)`.
More concisely: If `α` and `β` have a preorder and `f : α → β` is strictly monotonic, then `f` is strictly monotonic on any subset `s` of `α`.
|
Monotone.ne_of_lt_of_lt_int
theorem Monotone.ne_of_lt_of_lt_int :
∀ {α : Type u} [inst : Preorder α] {f : ℤ → α},
Monotone f → ∀ (n : ℤ) {x : α}, f n < x → x < f (n + 1) → ∀ (a : ℤ), f a ≠ x
The theorem `Monotone.ne_of_lt_of_lt_int` states that for any preorder `α`, and any monotone function `f` from integers to `α`, if an element `x` of `α` lies strictly between `f(n)` and `f(n+1)` for some integer `n`, then `x` does not lie in the range of `f`. That is, there is no integer `a` such that `f(a) = x`.
More concisely: If `f` is a monotonic function from integers to a preorder `α`, and there exists an integer `n` such that `x` is strictly between `f(n)` and `f(n+1)`, then `x` is not in the range of `f`.
|
StrictAnti.antitone
theorem StrictAnti.antitone :
∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β}, StrictAnti f → Antitone f
The theorem `StrictAnti.antitone` states that for any function `f` mapping from a type `α` to a type `β`, where `α` is a partially ordered set and `β` is a preordered set, if `f` is strictly antitone (i.e., for any `a` and `b` in `α` where `a < b`, it implies `f(b) < f(a)`), then `f` is also antitone (i.e., for any `a` and `b` in `α` where `a ≤ b`, it implies `f(b) ≤ f(a)`).
More concisely: If `f` is a strictly antitone function from a partially ordered set `α` to a preordered set `β`, then `f` is antitone. (That is, for all `a ≤ b` in `α`, `f(b) ≤ f(a)`.)
|
AntitoneOn.dual
theorem AntitoneOn.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
AntitoneOn f s → AntitoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
This theorem, which is an alias of the reverse direction of `antitoneOn_dual_iff`, states that for any two types `α` and `β` with preorders, a function `f` from `α` to `β`, and a set `s` of type `α`, if `f` is antitone (i.e., it is a decreasing function) on `s`, then the composition of `OrderDual.toDual`, `f`, and `OrderDual.ofDual` (in that order) is also antitone on `s`. In other words, if `f` reverses the order of elements in `s`, then the same property holds even if we consider the dual order on the domain and range of `f`. Here, `OrderDual.toDual` and `OrderDual.ofDual` are identity functions that convert a type to its dual order and back, respectively.
More concisely: If `f` is an antitone function from preordered set `α` to preordered set `β` and `s` is a subset of `α`, then the composition of `OrderDual.toDual`, `f`, and `OrderDual.ofDual` is antitone on `s`.
|
injective_of_le_imp_le
theorem injective_of_le_imp_le :
∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] (f : α → β),
(∀ {x y : α}, f x ≤ f y → x ≤ y) → Function.Injective f
The theorem `injective_of_le_imp_le` is a statement about a function `f` from a partially ordered type `α` to a preordered type `β`. It says that if for all elements `x` and `y` of `α`, the statement "`f(x)` is less than or equal to `f(y)`" implies that "`x` is less than or equal to `y`", then the function `f` is injective. In other words, if `f` preserves the order structure from `α` to `β`, then there cannot be distinct elements in `α` that get mapped to the same element in `β`, which is the definition of an injective function.
More concisely: If a function from a partially ordered type to a preordered type preserves order relations, then it is injective.
|
MonotoneOn.reflect_lt
theorem MonotoneOn.reflect_lt :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
MonotoneOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → f a < f b → a < b
This theorem, `MonotoneOn.reflect_lt`, states that for any types `α` and `β` where `α` is a linear order and `β` is a preorder, if a function `f` from `α` to `β` is monotone on a set `s` of `α`, then for any two elements `a` and `b` in `s`, if `f(a)` is less than `f(b)`, it must be the case that `a` is less than `b`. Essentially, it asserts that the ordering of the function values reflects the ordering of the inputs for any two elements in the set where the function is monotone.
More concisely: If `f` is a monotone function from a linearly ordered type `α` to a preordered type `β`, and `a` and `b` are in `α` with `a` less than `b` and `f(a)` less than `f(b)`, then `a` is less than `b` in `α`.
|
StrictAnti.dual_left
theorem StrictAnti.dual_left :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
StrictAnti f → StrictMono (f ∘ ⇑OrderDual.ofDual)
This theorem states that for any two types `α` and `β` equipped with the structure of a Preorder, if a function `f` from `α` to `β` is strictly antitone (meaning that `a < b` implies `f b < f a`), then the function composed with `f` and `OrderDual.ofDual` (which is the identity on the dual order of `α`) is strictly monotone (meaning that `a < b` implies `f a < f b`). This theorem essentially asserts a relationship between a strictly antitone function and its dual, the strictly monotone function.
More concisely: If `f` is a strictly antitone function between preordered types `α` and `β`, then `OrderDual.ofDual ∘ f` is a strictly monotone function.
|