lt_max_of_lt_left
theorem lt_max_of_lt_left : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < b → a < max b c
This theorem states that for any type `α` that has a linear order, if `a` is less than `b`, then `a` is also less than the maximum of `b` and `c`. This holds for any three values `a`, `b` and `c` of that type. In terms of algebra, if we have `a < b`, it's guaranteed that `a < max(b, c)`.
More concisely: For any type `α` with a linear order, if `a` is less than `b`, then `a` is also less than the maximum of `b` and `c`. In symbols: `a < b` implies `a < max b c`.
|
Mathlib.Order.MinMax._auxLemma.1
theorem Mathlib.Order.MinMax._auxLemma.1 :
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, (c ≤ min a b) = (c ≤ a ∧ c ≤ b)
This theorem states that for any type `α` that has a linear order, and for any three elements `a`, `b`, and `c` of type `α`, `c` is less than or equal to the minimum of `a` and `b` if and only if `c` is less than or equal to `a` and `c` is less than or equal to `b`. In LaTeX mathematics, this would be expressed as $c \leq \min(a, b) \iff (c \leq a \land c \leq b)$.
More concisely: For any linear order type `α` and elements `a`, `b`, `c` of type `α`, `c` is the minimum of `a` and `b` if and only if `c` is less than or equal to both `a` and `b`.
|
Antitone.map_min
theorem Antitone.map_min :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {a b : α},
Antitone f → f (min a b) = max (f a) (f b)
The theorem `Antitone.map_min` states that for any two types `α` and `β` with a linear order, given an antitone function `f` from `α` to `β` and any two elements `a` and `b` of type `α`, the result of applying `f` to the minimum of `a` and `b` is equal to the maximum of the results of applying `f` to `a` and `b` individually. In other words, if `f` is a function that preserves the order in the opposite direction, then applying `f` switches the roles of `min` and `max`.
More concisely: For any antitone function $f$ between linearly ordered types $\alpha$ and $\beta$, and any $a, b \in \alpha$, we have $f(\min(a, b)) = \max(f(a), f(b))$.
|
min_le_max
theorem min_le_max : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, min a b ≤ max a b
This theorem states that in a linearly ordered type `α`, for any two elements `a` and `b` of that type, the minimum of `a` and `b` is less than or equal to the maximum of `a` and `b`. In mathematical terms, this corresponds to the fact that for any two elements in a set that is linearly ordered (like the real numbers, for example), the smaller one is always less than or equal to the larger one.
More concisely: In a linearly ordered type, the minimum of any two elements is less than or equal to their maximum.
|
min_cases
theorem min_cases : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a := by
sorry
The theorem `min_cases` states that for any two elements `a` and `b` of a type `α` which has a linear order, one of the following two situations must hold: either the minimum of `a` and `b` is `a` and `a` is less than or equal to `b`, or the minimum of `a` and `b` is `b` and `b` is strictly less than `a`. This theorem is useful in proofs involving inequalities, where it helps automate the process of using the `linarith` tactic.
More concisely: For any elements `a` and `b` in a linearly ordered type `α`, either `a ≤ b` and `a` is the minimum, or `b < a` and `b` is the minimum.
|
Monotone.map_max
theorem Monotone.map_max :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {a b : α},
Monotone f → f (max a b) = max (f a) (f b)
The theorem `Monotone.map_max` states that, for any types `α` and `β` that have a linear order, and for any function `f` from `α` to `β`, if `f` is a monotone function, then the result of applying `f` to the maximum of two elements `a` and `b` of type `α` is equivalent to the maximum of the results of applying `f` to `a` and `b` individually. In mathematical terms, given `a, b ∈ α` and a monotone function `f: α → β`, we have `f(max(a, b)) = max(f(a), f(b))`.
More concisely: For any types `α` and `β` with a linear order, and any monotone function `f: α → β`, `f(max(a, b)) = max(f(a), f(b))` for all `a, b ∈ α`.
|
Mathlib.Order.MinMax._auxLemma.10
theorem Mathlib.Order.MinMax._auxLemma.10 : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, (min a b = b) = (b ≤ a)
This theorem, `Mathlib.Order.MinMax._auxLemma.10`, states that for any type `α` which has a linear order, and any two members `a` and `b` of that type, the minimum of `a` and `b` equals `b` if and only if `b` is less than or equal to `a`. In other words, `b` is the minimum of `a` and `b` when it is not greater than `a`.
More concisely: For any type with a linear order, the minimum of two elements is the smaller one. (Equivalently, element `b` is the minimum of `a` and `b` if and only if `b` is less than or equal to `a`. )
|
Mathlib.Order.MinMax._auxLemma.6
theorem Mathlib.Order.MinMax._auxLemma.6 :
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, (a < max b c) = (a < b ∨ a < c)
This theorem states that for any type `α` which has a linear order, and for any three elements `a`, `b`, `c` of this type, `a` is less than the maximum of `b` and `c` if and only if `a` is less than `b` or `a` is less than `c`. Specifically, `max b c` returns the maximum number between `b` and `c`, so `a` being less than this maximum is equivalent to `a` being less than at least one of `b` or `c`.
More concisely: For any type with a linear order, element `a` is less than the maximum of elements `b` and `c` if and only if `a` is less than `b` or less than `c`.
|
max_cases
theorem max_cases : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), max a b = a ∧ b ≤ a ∨ max a b = b ∧ a < b := by
sorry
This theorem states that for any two elements `a` and `b` in a linear order, one of the two conditions must be true: either the maximum of `a` and `b` is `a` and `b` is less than or equal to `a`, or the maximum of `a` and `b` is `b` and `a` is strictly less than `b`. This theorem is used for automating linear arithmetic in inequalities.
More concisely: For any two elements `a` and `b` in a linear order, either `a ≥ b` and `b ≤ a`, or `a < b` and `b ≥ a`.
|
Mathlib.Order.MinMax._auxLemma.3
theorem Mathlib.Order.MinMax._auxLemma.3 :
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, (min a b ≤ c) = (a ≤ c ∨ b ≤ c)
This theorem states that for any type `α` that has a linear order, and for any three elements `a`, `b`, and `c` of this type, the minimum of `a` and `b` is less than or equal to `c` if and only if `a` is less than or equal to `c` or `b` is less than or equal to `c`. In other words, it is saying that `c` is greater than or equal to the smallest of `a` and `b` if `c` is greater than or equal to either `a` or `b`.
More concisely: For any linear order type `α` and elements `a`, `b`, `c` of `α`, `min a b ≤ c` if and only if `a ≤ c` or `b ≤ c`.
|
max_le_iff
theorem max_le_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, max a b ≤ c ↔ a ≤ c ∧ b ≤ c
This theorem states that for any type `α` that has a linear order, and given three elements `a`, `b` and `c` of type `α`, the maximum of `a` and `b` is less than or equal to `c` if and only if both `a` and `b` are less than or equal to `c`. In other words, in a linearly ordered set, an element `c` is greater than or equal to the maximum of `a` and `b` if and only if `c` is greater than or equal to both `a` and `b`.
More concisely: In a linearly ordered set, the maximum of two elements is equal to each element when both elements are less than or equal to the maximum.
|
Mathlib.Order.MinMax._auxLemma.2
theorem Mathlib.Order.MinMax._auxLemma.2 :
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, (a ≤ max b c) = (a ≤ b ∨ a ≤ c)
This theorem states that for any type `α` that is a linear order, and for any three elements `a`, `b`, and `c` of this type, `a` is less than or equal to the maximum of `b` and `c` if and only if `a` is less than or equal to `b` or `a` is less than or equal to `c`. This theorem generalizes the intuitive property of "max" function from number theory to any linearly ordered set.
More concisely: For any linear order `α` and elements `a`, `b`, `c` in `α`, `a` is less than or equal to the maximum of `b` and `c` if and only if `a` is less than or equal to both `b` and `c`.
|
le_max_iff
theorem le_max_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a ≤ max b c ↔ a ≤ b ∨ a ≤ c
This theorem, `le_max_iff`, states that for any type `α` that has a linear order, and for any three elements `a`, `b`, `c` of that type, `a` is less than or equal to the maximum of `b` and `c` if and only if `a` is less than or equal to `b` or `a` is less than or equal to `c`. In other words, the value `a` is no larger than the bigger one of `b` and `c` if `a` is no larger than at least one of `b` and `c`.
More concisely: For any type `α` with a linear order and any elements `a`, `b`, `c` of `α`, `a ≤ max b c` if and only if `a ≤ b` or `a ≤ c`.
|
Monotone.map_min
theorem Monotone.map_min :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {a b : α},
Monotone f → f (min a b) = min (f a) (f b)
The theorem `Monotone.map_min` states that for any types `α` and `β` with a linear order, a function `f` from `α` to `β`, and any elements `a` and `b` of `α`, the following holds: if `f` is a monotone function (i.e., a function where `a ≤ b` implies `f(a) ≤ f(b)`), then the application of `f` to the minimum of `a` and `b` is equal to the minimum of `f(a)` and `f(b)`. In other words, a monotone function preserves the operation of taking the minimum.
More concisely: If `f` is a monotonic function from a type `α` with a linear order to another type `β` also with a linear order, then `f(min(a, b)) = min(f(a), f(b))` for all `a, b ∈ α`.
|
Mathlib.Order.MinMax._auxLemma.7
theorem Mathlib.Order.MinMax._auxLemma.7 :
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, (min a b < c) = (a < c ∨ b < c)
This theorem, called `Mathlib.Order.MinMax._auxLemma.7`, states that for any type `α` under a linear order, and any three values `a`, `b`, and `c` of type `α`, the condition that the minimum of `a` and `b` is less than `c` holds true if and only if either `a` is less than `c` or `b` is less than `c`. This is a fundamental property of minimum values in any ordered set.
More concisely: For any type under a linear order, the minimum of two elements is less than a third element if and only if one of the first two elements is less than the third.
|
max_eq_right_iff
theorem max_eq_right_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, max a b = b ↔ a ≤ b
This theorem, `max_eq_right_iff`, states that for any given type `α` with a linear order, and any two elements `a` and `b` of type `α`, the maximum of `a` and `b` is `b` if and only if `a` is less than or equal to `b`. In other words, it provides a condition under which `b` is the maximum of `a` and `b` in a linearly ordered set.
More concisely: For any type `α` with a linear order, `a` and `b` in `α`, `b` is the maximum of `a` and `b` if and only if `a ≤ b`.
|
lt_max_iff
theorem lt_max_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < max b c ↔ a < b ∨ a < c
This theorem, `lt_max_iff`, states that for any type `α` that has a linear order, and for any three elements `a`, `b`, and `c` of this type, `a` is less than the maximum of `b` and `c` if and only if `a` is less than `b` or `a` is less than `c`. This theorem essentially captures the property of maximum in the context of linear orders.
More concisely: For any type `α` with a linear order and any elements `a`, `b`, `c` of `α`, `a` is less than the maximum of `b` and `c` if and only if `a` is less than `b` or `a` is less than `c`.
|
Antitone.map_max
theorem Antitone.map_max :
∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {a b : α},
Antitone f → f (max a b) = min (f a) (f b)
The theorem `Antitone.map_max` states that for any types `α` and `β` with a linear order, and any function `f` from `α` to `β` which is antitone (meaning that if `a ≤ b` then `f b ≤ f a`), when this function `f` is applied to the maximum of two elements `a` and `b` from `α`, it gives the minimum of the function `f` applied to `a` and `b`. In other words, if `f` is an antitone function, then `f` of max(`a`,`b`) is equal to min(`f(a)`,`f(b)`).
More concisely: For any antitone function $f$ between linearly ordered types $\alpha$ and $\beta$, we have $f(\max(a, b)) = \min(f(a), f(b))$.
|
min_le_iff
theorem min_le_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, min a b ≤ c ↔ a ≤ c ∨ b ≤ c
This theorem states that for a given linear ordering of some type `α`, the minimum of two elements `a` and `b` is less than or equal to a third element `c` if and only if either `a` is less than or equal to `c` or `b` is less than or equal to `c`. In mathematical terms, this theorem expresses that `min(a, b) ≤ c` is equivalent to `a ≤ c ∨ b ≤ c`.
More concisely: For all linear order types `α`, the minimum of two elements `a` and `b` is less than or equal to a third element `c` if and only if `a` is less than or equal to `c` or `b` is less than or equal to `c`. In mathematical notation: `min(a, b) ≤ c ↔ a ≤ c ∨ b ≤ c`.
|
max_min_distrib_left
theorem max_min_distrib_left :
∀ {α : Type u} [inst : LinearOrder α] (a b c : α), max a (min b c) = min (max a b) (max a c)
This theorem states that for any type `α` that obeys the laws of linear order, and any elements `a`, `b`, and `c` of this type, the maximum of `a` and the minimum of `b` and `c` is equal to the minimum of the maximum of `a` and `b` and the maximum of `a` and `c`. This is a statement about the distributive properties of the `max` and `min` functions in a linearly ordered set.
More concisely: For all linearly ordered types `α` and elements `a, b, c` of `α`, the maximum of `a` and the minimum of `b` and `c` equals the minimum of the maximum of `a` and `b`, and the maximum of `a` and `c` (distributivity of `max` and `min` in a linearly ordered set).
|
min_eq_left_iff
theorem min_eq_left_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, min a b = a ↔ a ≤ b
This theorem states that for any given type `α` that has a linear order, the minimum of two elements `a` and `b` of this type will be `a` if and only if `a` is less than or equal to `b`. In other words, it provides a condition under which the minimum of two elements in a linearly ordered set is the first of those elements.
More concisely: For any linearly ordered type `α`, the minimum element is equal to the least element with respect to the order relation. In other words, `a` is the minimum of `a` and `b` if and only if `a ≤ b` holds in the order relation.
|
Mathlib.Order.MinMax._auxLemma.4
theorem Mathlib.Order.MinMax._auxLemma.4 :
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, (max a b ≤ c) = (a ≤ c ∧ b ≤ c)
This theorem, `Mathlib.Order.MinMax._auxLemma.4`, states that for any type `α` that has a linear order, and any three elements `a`, `b`, and `c` of type `α`, the maximum of `a` and `b` is less than or equal to `c` if and only if both `a` and `b` are less than or equal to `c`. This means that for `c` to be greater than or equal to the maximum of `a` and `b`, it must be greater than or equal to both `a` and `b` individually.
More concisely: For any type with a linear order, the maximum of two elements is less than or equal to a third element if and only if the first two elements are less than or equal to the third.
|
le_max_of_le_left
theorem le_max_of_le_left : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a ≤ b → a ≤ max b c
This theorem states that for any type `α` that has a linear order, and any three elements `a`, `b`, and `c` in this type, if `a` is less than or equal to `b`, then `a` is also less than or equal to the maximum of `b` and `c`. In other words, in terms of general mathematics, if a ≤ b, then a is also less than or equal to max(b, c) for any linearly ordered set.
More concisely: For any linearly ordered type `α` and elements `a`, `b`, `c` in `α`, if `a ≤ b`, then `a ≤ max b c`.
|
max_choice
theorem max_choice : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), max a b = a ∨ max a b = b
This theorem, `max_choice`, states that for any type `α` that has a linear order, and for any two elements `a` and `b` of this type, the maximum of `a` and `b` is either `a` or `b`. In simpler words, this theorem says that for any two numbers `a` and `b`, the larger (or maximum) of the two is always either `a` or `b`.
More concisely: For any type `α` with a linear order, the maximum of two elements `a` and `b` is equal to `a` if `a` is greater than or equal to `b`, and equal to `b` otherwise.
|
lt_max_of_lt_right
theorem lt_max_of_lt_right : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < c → a < max b c
This theorem states that for any type `α` that has a linear ordering, if a certain value `a` of type `α` is less than another value `c` of the same type, then `a` is also less than the maximum of `b` and `c`, where `b` and `c` are also values of type `α`. This is a fairly intuitive result, as if `a` is less than `c`, then `a` is certainly less than the highest value between `b` and `c`.
More concisely: For any linear ordered type `α`, if `a` is less than `c` in `α`, then `a` is also less than the maximum of `b` and `c` in `α`.
|
le_max_of_le_right
theorem le_max_of_le_right : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a ≤ c → a ≤ max b c
This theorem, `le_max_of_le_right`, states that for any linearly ordered type `α` and any three elements `a`, `b`, and `c` of this type, if `a` is less than or equal to `c`, then `a` is also less than or equal to the maximum of `b` and `c`. This theorem captures a fundamental property of "max" operation in the context of ordered types.
More concisely: For any linearly ordered type α and elements a, b, c of α, if a ≤ c then a ≤ max(b c).
|
max_lt_iff
theorem max_lt_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, max a b < c ↔ a < c ∧ b < c
This theorem states that for any given type `α` under a linear order, the maximum of two elements `a` and `b` is less than a third element `c` if and only if both `a` and `b` are less than `c`. In other words, `c` is greater than both `a` and `b`, if and only if `c` is greater than their maximum.
More concisely: For any type `α` under a linear order, `c` is greater than the maximum of `a` and `b` if and only if `c` is greater than both `a` and `b`.
|
Mathlib.Order.MinMax._auxLemma.9
theorem Mathlib.Order.MinMax._auxLemma.9 : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, (min a b = a) = (a ≤ b)
This theorem, `Mathlib.Order.MinMax._auxLemma.9`, states that for any type `α` which has a `LinearOrder` instance, and for any two elements `a` and `b` of this type, the condition that the minimum of `a` and `b` is equal to `a` is equivalent to the condition that `a` is less than or equal to `b`. In other words, `min(a, b) = a` if and only if `a ≤ b`.
More concisely: For any type with a LinearOrder instance, the minimum of two elements is equal to the first element if and only if the first element is less than or equal to the second.
|
max_le_max
theorem max_le_max : ∀ {α : Type u} [inst : LinearOrder α] {a b c d : α}, a ≤ c → b ≤ d → max a b ≤ max c d
This theorem, named `max_le_max`, states that for any linearly ordered type `α`, if `a` and `b` are two elements of this type such that `a` is less than or equal to `c` and `b` is less than or equal to `d`, then the maximum of `a` and `b` is less than or equal to the maximum of `c` and `d`. In mathematical terms, this could be written as: for any $a, b, c, d \in \alpha$, if $a \leq c$ and $b \leq d$, then $\max(a, b) \leq \max(c, d)$.
More concisely: For any linearly ordered type α and elements a, b, c, d ∈ α, if a ≤ c and b ≤ d, then max(a, b) ≤ max(c, d).
|
min_le_min
theorem min_le_min : ∀ {α : Type u} [inst : LinearOrder α] {a b c d : α}, a ≤ c → b ≤ d → min a b ≤ min c d
This theorem states that for any linearly ordered type `α` and any four elements `a`, `b`, `c` and `d` of that type, if `a` is less than or equal to `c` and `b` is less than or equal to `d`, then the minimum of `a` and `b` is less than or equal to the minimum of `c` and `d`. This theorem is a generalization of the property of the min function in order theory, asserting the monotonicity of the min function in each of its arguments.
More concisely: For any linearly ordered type `α` and elements `a, b, c, d` of `α`, if `a ≤ c` and `b ≤ d`, then `min {a, b} ≤ min {c, d}`.
|
lt_min_iff
theorem lt_min_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < min b c ↔ a < b ∧ a < c
This theorem states that for all types `α` that have a linear order, and for all instances of this type `a`, `b`, and `c`, `a` is less than the minimum of `b` and `c` if and only if `a` is less than `b` and `a` is less than `c`. In other words, an element is less than the minimum of two other elements if and only if it is less than both of these elements.
More concisely: For all types with a linear order and elements `a`, `b`, `c`, if `a` is less than the minimum of `b` and `c`, then `a` is less than both `b` and `c`.
|
Mathlib.Order.MinMax._auxLemma.5
theorem Mathlib.Order.MinMax._auxLemma.5 :
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, (a < min b c) = (a < b ∧ a < c)
This theorem states that for any type `α` that has a linear order, and for any three instances `a`, `b`, and `c` of this type, the statement `a` is less than the minimum of `b` and `c` is equivalent to the conjunction of the statements `a` is less than `b` and `a` is less than `c`. In other words, in a linear order, a value is less than the minimum of two other values if and only if it is less than each of those values.
More concisely: For any linear order type `α`, and elements `a`, `b`, `c` of type `α`, `a` is less than the minimum of `b` and `c` if and only if `a` is less than both `b` and `c`.
|
Mathlib.Order.MinMax._auxLemma.8
theorem Mathlib.Order.MinMax._auxLemma.8 :
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, (max a b < c) = (a < c ∧ b < c)
This theorem states that for any type `α` that has an instance of `LinearOrder`, and for any three elements `a`, `b`, `c` of this type, the maximum of `a` and `b` being less than `c` is equivalent to both `a` and `b` being less than `c`. In other words, if `c` is greater than both `a` and `b`, then `c` is also greater than the maximum of `a` and `b`, and vice-versa.
More concisely: For any type `α` with a `LinearOrder` instance, the maximum of `a` and `b` in `α` is equal to `c` if and only if both `a` and `b` are less than `c`.
|