max_assoc
theorem max_assoc : ∀ {α : Type u} [inst : LinearOrder α] (a b c : α), max (max a b) c = max a (max b c)
This theorem, `max_assoc`, states that for any type `α` that has a linear order, the maximum of three elements `a`, `b`, and `c` is associative. In other words, taking the maximum of `a` and `b` first, and then the maximum with `c`, is the same as taking the maximum of `b` and `c` first, and then the maximum with `a`. This can be mathematically expressed as: max(max(a, b), c) = max(a, max(b, c)).
More concisely: For all types `α` with a linear order, the association holds: max(max(a, b), c) = max(a, max(b, c)).
|
Mathlib.Init.Order.LinearOrder._auxLemma.1
theorem Mathlib.Init.Order.LinearOrder._auxLemma.1 : ∀ {α : Type u} [inst : Preorder α] (a : α), (a ≤ a) = True := by
sorry
This theorem states that, for any type `α` with a preorder, any element `a` of `α` is less than or equal to itself. In mathematical notation, this is expressing the reflexivity of the order relation: for all `a`, `a ≤ a` is always true.
More concisely: For any preordered type `α`, every element `a` satisfies `a ≤ a`.
|
eq_max
theorem eq_max :
∀ {α : Type u} [inst : LinearOrder α] {a b c : α},
a ≤ c → b ≤ c → (∀ {d : α}, a ≤ d → b ≤ d → c ≤ d) → c = max a b
This theorem states that for any linearly ordered type `α`, and for any three elements `a`, `b`, `c` of this type, if `a` and `b` are both less than or equal to `c`, and `c` is less than or equal to any `d` such that `a` and `b` are both less than or equal to `d`, then `c` is equal to the maximum of `a` and `b`. In simple terms, it asserts that `c` is the maximum of `a` and `b` if `c` is greater than or equal to both of them and there is no other element greater than `c` to which both `a` and `b` are less than or equal to.
More concisely: If `α` is linearly ordered and `a`, `b`, `c` are in `α` such that `a` and `b` are less than or equal to `c`, and for all `d` in `α` with `a` and `b` less than or equal to `d`, we have `c` = max {`a`, `b`}, then `c` is the maximum of `a` and `b`.
|
max_eq_right_of_lt
theorem max_eq_right_of_lt : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, a < b → max a b = b
This theorem, `max_eq_right_of_lt`, states that for any type `α` equipped with a `LinearOrder` (which is a mathematical structure that allows us to compare elements), given two elements `a` and `b` of this type, if `a` is strictly less than `b`, then the maximum of `a` and `b` is `b`. Essentially, it's saying that if you have two things and the first one is smaller, then the biggest one is the second one.
More concisely: For all types `α` with a `LinearOrder` and all `a` and `b` in `α`, if `a` is strictly less than `b`, then `max a b = b`.
|
lt_min
theorem lt_min : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < b → a < c → a < min b c
This theorem, `lt_min`, asserts that for any type `α` that has a linear order, and for any three elements `a`, `b`, and `c` of that type, if `a` is less than `b` and `a` is less than `c`, then `a` is less than the minimum of `b` and `c`. Essentially, it's saying that if `a` is less than two other elements, it's also less than the smallest of those two elements.
More concisely: For all types `α` with a linear order and all `a`, `b`, `c` in `α`, if `a` is less than `b` and `a` is less than `c`, then `a` is less than the minimum of `b` and `c`. In mathematical notation: `a < b ∧ a < c → a < min b c`.
|
min_self
theorem min_self : ∀ {α : Type u} [inst : LinearOrder α] (a : α), min a a = a
The theorem `min_self` states that for all types `α` which have a `LinearOrder` instance, the minimum of a value `a` and itself is always `a`. In other words, for any type `α` that can be ordered in a linear fashion (like integers or real numbers), if you compare a value with itself, the smaller value is always going to be the value itself.
More concisely: For all types `α` with a `LinearOrder`, the reflexive property holds: `a ≤ a` for all `a` in `α`.
|
max_lt
theorem max_lt : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < c → b < c → max a b < c
This theorem, `max_lt`, states that for any type `α` that has a linear order, and any three elements `a`, `b`, and `c` of type `α`, if `a` is less than `c` and `b` is less than `c`, then the maximum value of `a` and `b` is also less than `c`. That is, in a linearly ordered set, if both `a` and `b` are less than `c`, then the maximum of `a` and `b` will also be less than `c`.
More concisely: If `α` is a linearly ordered type and `a`, `b`, `c` are elements of `α` with `a < c` and `b < c`, then `max {a, b} < c`.
|
max_eq_right
theorem max_eq_right : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, a ≤ b → max a b = b
This theorem, `max_eq_right`, states that for any type `α` which has a linear order, given any two elements `a` and `b` of type `α`, if `a` is less than or equal to `b`, then the maximum of `a` and `b` is `b`. In other words, in a linearly ordered set, if one element is not greater than the other, the maximum of the two is the other element.
More concisely: For any linearly ordered type `α` and elements `a` and `b` of `α`, if `a` is less than or equal to `b`, then the maximum of `a` and `b` equals `b`.
|
eq_min
theorem eq_min :
∀ {α : Type u} [inst : LinearOrder α] {a b c : α},
c ≤ a → c ≤ b → (∀ {d : α}, d ≤ a → d ≤ b → d ≤ c) → c = min a b
This theorem states that for any type `α` that has a linear order, given three instances `a`, `b`, and `c` of this type, if `c` is less than or equal to both `a` and `b`, and for all `d` of type `α`, if `d` is less than or equal to `a` and `b`, then `d` is also less than or equal to `c`, it follows that `c` is equal to the minimum of `a` and `b`. In terms of mathematical language, given $c \leq a$ and $c \leq b$ and for all $d$, $d \leq a$ and $d \leq b$ implies $d \leq c$, then $c = \min(a, b)$.
More concisely: If `α` is a type with a linear order and `c` is between `a` and `b` with `c` less than or equal to all `d` in `α` that are less than or equal to `a` and `b`, then `c` is the minimum of `a` and `b`. In mathematical notation: $c \in \{\min(a, b)\} \iff c \leq a, c \leq b \land \forall d \in \alpha, d \leq a, d \leq b \implies d \leq c$.
|
max_def
theorem max_def : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), max a b = if a ≤ b then b else a
This theorem, `max_def`, states that for all types `α` (assuming `α` has an instance of `LinearOrder`, which provides an ordering for elements of `α`), the maximum of any two elements `a` and `b` of type `α` is determined as follows: If `a` is less than or equal to `b`, then the maximum is `b`; otherwise, the maximum is `a`.
More concisely: For any type `α` with a LinearOrder instance, the maximum of `a` and `b` in `α` is `a` if `a` is greater than `b`, and is `b` otherwise.
|
min_def
theorem min_def : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), min a b = if a ≤ b then a else b
This theorem states that for every type `α` that has a linear order, the minimum of two elements `a` and `b` of type `α` is defined as `a` if `a` is less than or equal to `b` and `b` otherwise. This theorem essentially provides a definition for the minimum function in the context of any ordered type.
More concisely: For any type `α` with a linear order, the minimum of `a` and `b` is `a` if `a ≤ b` and `b` otherwise.
|
min_le_right
theorem min_le_right : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), min a b ≤ b
This theorem states that for any type `α` that has a linear order, the minimum of any two elements `a` and `b` of this type is always less than or equal to `b`. This is a general property of minimum operations in ordered types.
More concisely: For any type `α` with a linear order, the minimum element is less than or equal to any other element.
|
max_le
theorem max_le : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a ≤ c → b ≤ c → max a b ≤ c
This is a theorem about the maximum operation in a Linear Ordered set. It states that for any type `α` equipped with a linear order, given any three elements `a`, `b`, and `c` of type `α`, if `a` is less than or equal to `c` and `b` is less than or equal to `c`, then the maximum of `a` and `b` is less than or equal to `c`. In the language of mathematics, this would be expressed as $\forall a, b, c \in \alpha . (a \leq c \land b \leq c) \Rightarrow max(a, b) \leq c$.
More concisely: For any linear order `α`, if `a` and `b` are both less than or equal to `c` in `α`, then `max(a, b)` is less than or equal to `c`.
|
max_self
theorem max_self : ∀ {α : Type u} [inst : LinearOrder α] (a : α), max a a = a
This theorem, `max_self`, states that for any type `α` that has a linear order, the maximum of any element `a` and itself is always `a`. In other words, for any `a` in a linearly ordered set, `max(a, a)` is always equal to `a`.
More concisely: For any type `α` with a linear order, the reflexivity property holds: for all `a` in `α`, `max a a = a`.
|
le_min
theorem le_min : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, c ≤ a → c ≤ b → c ≤ min a b
This theorem, `le_min`, establishes a certain property of the `min` function in the context of linearly ordered types. Given any type `α` that has a linear order, and any three elements `a`, `b`, and `c` of this type, if `c` is less than or equal to `a` and `c` is less than or equal to `b`, then `c` is also less than or equal to the minimum of `a` and `b`. Essentially, this is a formalization of the intuitive understanding of the minimum function and less-than-or-equal-to relation in mathematics.
More concisely: If `α` is a linearly ordered type and `a`, `b`, `c` are elements of `α` with `c` less than or equal to both `a` and `b`, then `c` is less than or equal to the minimum of `a` and `b` (i.e., `min a b`).
|
min_comm
theorem min_comm : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), min a b = min b a
This theorem, named `min_comm`, states that for any type `α` that has a `LinearOrder` instance (meaning the type has a linear, or total, order), the minimum of two elements `a` and `b` of type `α` is the same regardless of the order in which `a` and `b` are considered. In other words, the operation of taking the minimum is commutative.
More concisely: For any type `α` with a linear order and any elements `a` and `b` of type `α`, `min a b` is equal to `min b a`.
|
le_max_left
theorem le_max_left : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), a ≤ max a b
This theorem, named `le_max_left`, states that for all types `α` that have a linear order, for any two elements `a` and `b` of type `α`, `a` is less than or equal to the maximum of `a` and `b`. In other words, for any two elements in a linearly ordered set, one of the elements is always less than or equal to the maximum of the two elements.
More concisely: For all types `α` with a linear order and any `a, b` in `α`, `a ≤ max a b`.
|
min_assoc
theorem min_assoc : ∀ {α : Type u} [inst : LinearOrder α] (a b c : α), min (min a b) c = min a (min b c)
This theorem, `min_assoc`, states that for any type `α` that has a linear order, the function `min` is associative. In other words, for any three elements `a`, `b`, and `c` of this type, computing the minimum of `a` and `b` first and then the minimum of the result with `c` yields the same result as computing the minimum of `b` and `c` first and then the minimum of `a` with the result. This is similar to the mathematical property that, for real numbers, `(a⊕b)⊕c = a⊕(b⊕c)`, where `⊕` represents the min operation.
More concisely: For any type `α` with a linear order, the function `min` is associative: `min a (min b c) = min (min a b) c`.
|
min_eq_left_of_lt
theorem min_eq_left_of_lt : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, a < b → min a b = a
This theorem states that for any type `α` that has a linear order, given two elements `a` and `b` of that type, if `a` is less than `b`, then the minimum of `a` and `b` is `a`. In other words, in a linearly ordered set, the minimum of two elements is the smaller one. This is a fundamental property of orderings and minimum operations.
More concisely: In a linearly ordered type, the minimum of two elements is the smaller one.
|
min_le_left
theorem min_le_left : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), min a b ≤ a
This theorem, `min_le_left`, states that for any given type `α` which has a linear order, and for any two elements `a` and `b` of that type, the minimum of `a` and `b` is less than or equal to `a`. This is a generalization of the well-known principle from mathematics that, for any two numbers, the smaller number (or the minimum) is always less than or equal to either of the two numbers.
More concisely: For any type `α` with a linear order and any elements `a` and `b` of `α`, `min a b ≤ a` holds.
|
min_eq_right
theorem min_eq_right : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, b ≤ a → min a b = b
The theorem `min_eq_right` states that for all types `α` that have a linear order, and for any two elements `a` and `b` of type `α`, if `b` is less than or equal to `a`, then the minimum of `a` and `b` is `b`. In other words, if `b` is less than or equal to `a`, then `b` is the smaller element.
More concisely: For all types with a linear order, the minimum of two elements is the smaller one.
|
le_max_right
theorem le_max_right : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), b ≤ max a b
This theorem, `le_max_right`, states that for all types `α` that have a linear ordering, for any two instances `a` and `b` of that type, `b` is less than or equal to the maximum of `a` and `b`. In other words, the theorem asserts that any element is always less than or equal to the maximum of itself and any other element of the same type, given that the type has a linear order structure.
More concisely: For all types `α` with a linear order and all `a, b : α`, we have `b <= max a b`.
|
min_eq_left
theorem min_eq_left : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, a ≤ b → min a b = a
This theorem, `min_eq_left`, states that for any type `α` which has a linear order, and for any two instances `a` and `b` of this type, if `a` is less than or equal to `b`, then the minimum of `a` and `b` is `a`. In other words, if `a` is not greater than `b`, it is the minimum of the two.
More concisely: For any type with a linear order, the minimum of two elements is the first if they are comparable and equal.
|
max_comm
theorem max_comm : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), max a b = max b a
This theorem states that for any type `α` which has a linear order structure, the maximum of two values `a` and `b` of this type is commutative. In other words, `max a b` is equal to `max b a` for any `a` and `b` from a type with a linear order. This mirrors the familiar property from mathematics that the maximum of two real numbers `a` and `b` is the same whether you write "max(a, b)" or "max(b, a)".
More concisely: For any type `α` with a linear order, the maximum of two elements `a` and `b` is commutative, i.e., `max a b = max b a`.
|
max_eq_left
theorem max_eq_left : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, b ≤ a → max a b = a
This theorem, `max_eq_left`, states that for any type `α` that has a linear ordering structure, given any two elements `a` and `b` of this type, if `b` is less than or equal to `a`, then the maximum of `a` and `b` is `a`. This is essentially a formal way in Lean of expressing the intuitive concept that if `b` is less than or equal to `a`, then `a` is the maximum of `a` and `b`.
More concisely: For all types `α` with a linear ordering and any `a` and `b` in `α`, if `b` is less than or equal to `a`, then `a` is the maximum of `a` and `b`. In mathematical notation: `a ≤ b → max a b = a`.
|
max_eq_left_of_lt
theorem max_eq_left_of_lt : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, b < a → max a b = a
This theorem, `max_eq_left_of_lt`, states that for any type `α` that has a linear order, given two objects `a` and `b` of this type, if `b` is less than `a`, then the maximum of `a` and `b` is equal to `a`. Essentially, it is proving the expected behavior of the `max` function: when applied to two arguments where the first is greater than the second, it will return the first argument.
More concisely: For all types `α` with a linear order and all `a b` in `α`, if `b` is less than `a`, then `max a b = a`.
|