LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Order.Basic

`Eq.trans_gt` theorem Eq.trans_gt : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, b = c → a < b → a < c This theorem, 'Eq.trans_gt', states that for any preorder set of elements of type 'α', if 'b' equals 'c' and 'a' is less than 'b', then 'a' is also less than 'c'. The term 'preorder' refers to a set where each pair of elements can be compared in a certain order. So, in essence, this theorem is saying that in a set where every element can be compared, if one element equals another and a third element is less than the first, the third element is also less than the second. More concisely: If `α` is a preorder type and `a < b = c`, then `a < c`.
`Ne.lt_or_lt` theorem Ne.lt_or_lt : ∀ {α : Type u} [inst : LinearOrder α] {x y : α}, x ≠ y → x < y ∨ y < x This theorem states that for any type `α` that has a linear order, given two elements `x` and `y` of type `α`, if `x` is not equal to `y`, then either `x` is less than `y` or `y` is less than `x`. It's essentially enforcing the trichotomy law for linearly ordered sets, which says that for any two elements in the set, one of them is either less than, equal to, or greater than the other. More concisely: For any linearly ordered type `α`, if `x` and `y` are distinct elements of `α`, then either `x` is less than `y` or `y` is less than `x`.
`StrongLT.le` theorem StrongLT.le : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → Preorder (π i)] {a b : (i : ι) → π i}, StrongLT a b → a ≤ b This theorem, referred to as an alias of `le_of_strongLT`, states that for all index types `ι` and any type `π` that is a function of the index type `ι`, if every element of type `π` has a preorder relation (i.e., it's reflexive and transitive), then for any two functions `a` and `b` from index `i` to `π i`, if `a` is strongly less than `b` (i.e., `a i < b i` for all `i`), then `a` is also less than or equal to `b` (`a ≤ b`). In other words, strong less-than relation implies a less-than-or-equal-to relation in a preorder context for any such functions `a` and `b`. More concisely: If `ι` is an index type and `π : ∀ i, Type` is a preorder type, then for all functions `a` and `b` from `ι` to `π`, if `a i` is strictly less than `b i` for all `i`, then `a ≤ b`.
`le_of_forall_ge_of_dense` theorem le_of_forall_ge_of_dense : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] {a₁ a₂ : α}, (∀ a₃ < a₁, a₃ ≤ a₂) → a₁ ≤ a₂ := by sorry The theorem `le_of_forall_ge_of_dense` states that for any type `α` that has a linear order and is densely ordered, given any two elements `a₁` and `a₂` of this type, if all elements `a₃` that are less than `a₁` are also less than or equal to `a₂`, then `a₁` is less than or equal to `a₂`. This theorem essentially captures the intuitive idea that if all elements less than `a₁` are bounded by `a₂`, then `a₁` must also be bounded by `a₂`. More concisely: If `α` is a densely ordered type with a linear order, then `a₁ ≤ a₂` holds if for all `a₃` with `a₃ < a₁`, we have `a₃ ≤ a₂`.
`le_of_forall_lt` theorem le_of_forall_lt : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, (∀ c < a, c < b) → a ≤ b This theorem states that for any type `α` that has a linear order, given two elements `a` and `b` of type `α`, if it holds true that all elements `c` less than `a` are also less than `b`, then `a` must be less than or equal to `b`. In mathematical terms, this theorem essentially establishes that if all elements smaller than `a` are also smaller than `b`, then `a` cannot be greater than `b`, i.e., `a` is less than or equal to `b`. More concisely: If `α` is a type with a linear order and for all `c` in `α` with `c < a`, it follows that `c < b`, then `a <= b`.
`lt_of_le_of_ne'` theorem lt_of_le_of_ne' : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≠ a → a < b This theorem, named `lt_of_le_of_ne'`, states that for any partially ordered set of type α, if an element `a` is less than or equal to another element `b` and `b` is not equal to `a`, then `a` is strictly less than `b`. This encapsulates the intuitive idea that if one element is not more than another and the two are not identical, then it must be that the first element is indeed less than the second. More concisely: If `a` is less than or equal to `b` and `a` is not equal to `b` in a partially ordered set, then `a` is strictly less than `b`.
`LE.le.eq_or_lt_dec` theorem LE.le.eq_or_lt_dec : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : DecidableRel fun x x_1 => x ≤ x_1] {a b : α}, a ≤ b → a = b ∨ a < b The theorem `LE.le.eq_or_lt_dec` is an alias of `Decidable.eq_or_lt_of_le`. It's a statement about partially ordered sets. Given any type `α` which has a partial order (`PartialOrder α`) and a decidable relation (`DecidableRel`) for whether one element is less than or equal to another, the theorem asserts that for any two elements `a` and `b` in this set, if `a` is less than or equal to `b` (`a ≤ b`), then either `a` equals `b` (`a = b`) or `a` is strictly less than `b` (`a < b`). More concisely: If `α` is a type with a partial order and a decidable `≤` relation, then for all `a` and `b` in `α`, if `a ≤ b` then `a = b` or `a < b`.
`LT.lt.trans_eq` theorem LT.lt.trans_eq : ∀ {α : Type u} {a b c : α} [inst : LT α], a < b → b = c → a < c This theorem, `LT.lt.trans_eq`, states that for any type `α` that has a less than (`<`) operation, if an element `a` is less than another element `b`, and `b` is equal to a third element `c`, then `a` is also less than `c`. This is essentially stating a property of transitivity for the less-than relation, where the transitivity also incorporates an equality. More concisely: If `a < b` and `b = c`, then `a < c` for any type `α` with a less-than relation `<`.
`LT.lt.not_lt` theorem LT.lt.not_lt : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → ¬b < a This theorem, `LT.lt.not_lt`, is an alias for `lt_asymm` in Lean. It states that for any type `α` equipped with a preorder relation, if one element `a` is strictly less than another element `b`, then it's not the case that `b` is strictly less than `a`. This rule essentially states that the "less than" relation is asymmetric, which is a defining feature of preorders. More concisely: If `a` is strictly less than `b` in a preorder relation on type `α`, then it is not the case that `b` is strictly less than `a`.
`le_iff_eq_or_lt` theorem le_iff_eq_or_lt : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b ↔ a = b ∨ a < b This theorem states that for any type `α` that has a partial order structure, given any two elements `a` and `b` of type `α`, `a` is less than or equal to `b` if and only if `a` is equal to `b` or `a` is strictly less than `b`. It essentially defines the 'less than or equal to' relation in terms of equality and strict less than relation. More concisely: For any partial order type `α`, `a ≤ b` if and only if `a = b` or `a < b`.
`le_trans'` theorem le_trans' : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, b ≤ c → a ≤ b → a ≤ c This theorem, `le_trans'`, states that for any preorder `α`, and any three elements `a`, `b`, and `c` from `α`, if `b` is less than or equal to `c` and `a` is less than or equal to `b`, then `a` is less than or equal to `c`. In other words, it formalizes the concept of transitivity in a preordered set. If you can go from `a` to `b` and from `b` to `c` in the order, then you can go directly from `a` to `c`. More concisely: If `α` is a preorder and `a`, `b`, `c` are elements of `α` with `a ≤ b` and `b ≤ c`, then `a ≤ c`.
`le_iff_le_iff_lt_iff_lt` theorem le_iff_le_iff_lt_iff_lt : ∀ {α : Type u} {β : Type u_3} [inst : LinearOrder α] [inst_1 : LinearOrder β] {a b : α} {c d : β}, (a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c) This theorem states that for any two types `α` and `β` that have a linear order, and for any elements `a`, `b` of type `α` and `c`, `d` of type `β`, the statement that `a` is less than or equal to `b` is equivalent to the statement that `c` is less than or equal to `d` if and only if the statement that `b` is less than `a` is equivalent to the statement that `d` is less than `c`. In mathematical terms, it's saying $(a \leq b) \Leftrightarrow (c \leq d)$ if and only if $(b < a) \Leftrightarrow (d < c)$. More concisely: For any linear orders on types `α` and `β`, the order relation `≤` on `α` is isomorphic to the order relation on `β` if and only if the reversed order relation `<` on `α` is isomorphic to the order relation on `β`.
`LT.lt.ne'` theorem LT.lt.ne' : ∀ {α : Type u} [inst : Preorder α] {x y : α}, x < y → y ≠ x This theorem states that for all types `α` that have a preorder structure, if `x` is less than `y`, then `y` is not equal to `x`. In other words, if one element is strictly less than another in a set with an order structure, then these two elements are distinct. More concisely: In a preordered type, if `x` is less than `y`, then `x ≠ y`.
`lt_imp_lt_of_le_imp_le` theorem lt_imp_lt_of_le_imp_le : ∀ {α : Type u} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} {c d : β}, (a ≤ b → c ≤ d) → d < c → b < a This theorem states that for any types `α` and `β` with a linear order and a preorder respectively, given two elements `a` and `b` of type `α`, and two elements `c` and `d` of type `β`, if it is the case that whenever `a` is less than or equal to `b` then `c` is less than or equal to `d`, then if `d` is less than `c`, it must be that `b` is less than `a`. Essentially, this theorem shows that a certain relationship between `a` and `b` implies a corresponding relationship between `c` and `d`, and vice versa. More concisely: If `α` is a type with a linear order, and `β` is a type with a preorder, if `a ≤ b` in `α` implies `c ≤ d` in `β`, then `d < c` implies `b < a`.
`LT.lt.lt_or_lt` theorem LT.lt.lt_or_lt : ∀ {α : Type u} [inst : LinearOrder α] {x y : α}, x < y → ∀ (z : α), x < z ∨ z < y This theorem states that for any linearly ordered type `α`, given three elements `x`, `y`, and `z` of this type, if `x` is less than `y`, then either `x` is less than `z` or `z` is less than `y`. Essentially, `z` must be greater than `x` or less than `y` given `x < y`, in any linear order. More concisely: For any linearly ordered type `α`, if `x < y` then `x <= z` or `z <= y`.
`eq_of_le_of_not_lt` theorem eq_of_le_of_not_lt : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → ¬a < b → a = b This theorem states that for any type `α` that has a partial order, if `a` and `b` are elements of type `α`, `a` is less than or equal to `b`, and it is not true that `a` is strictly less than `b`, then `a` must be equal to `b`. The proof is left as an exercise. This theorem essentially encapsulates the relationship between the less-than-or-equal-to relation (`≤`), the strictly-less-than relation (`<`), and the equality relation (`=`) in a partial order. More concisely: In a partially ordered type, if `a` is less than or equal to `b` and not strictly less than `b`, then `a` equals `b`.
`LT.lt.le` theorem LT.lt.le : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → a ≤ b This theorem, `LT.lt.le`, states that for any preorder `α`, and for any two elements `a` and `b` of this type, if `a` is less than `b` (`a < b`), then `a` is also less than or equal to `b` (`a ≤ b`). In other words, it confirms that less than implies less than or equal to in the context of a preorder. This is a fundamental property of ordered sets in mathematics. More concisely: In a preorder, if `a` is less than `b` (`a < b`), then `a` is also less than or equal to `b` (`a ≤ b`).
`Function.const_lt_const` theorem Function.const_lt_const : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Nonempty β] {a b : α}, Function.const β a < Function.const β b ↔ a < b The theorem `Function.const_lt_const` states that for any types `α` and `β`, where `α` has a preorder structure and `β` is nonempty, and for any elements `a` and `b` of type `α`, the constant function of type `β → α` with value `a` is less than the constant function with value `b` if and only if `a` is less than `b` under the preorder on `α`. In simpler terms, it means that the inequality relationship between two constants `a` and `b` is preserved when these constants are used as the values of constant functions. More concisely: For any preordered types `α` and non-empty `β`, and elements `a` and `b` of `α`, the constant function `λ (x : β), a` is less than the constant function `λ (x : β), b` in the function preorder if and only if `a` is less than `b` in the preorder on `α`.
`Mathlib.Order.Basic._auxLemma.1` theorem Mathlib.Order.Basic._auxLemma.1 : ∀ {α : Type u} [inst : Preorder α] (a : α), (a ≤ a) = True This theorem states that for any type `α` which has a preorder structure, any element `a` from that type is less than or equal to itself. In math terms, it's confirming the reflexivity property of the preorder, i.e., ∀a in α, a ≤ a, which is always true by definition of a preorder. More concisely: For any preorder type `α`, every element `a` satisfies `a ≤ a`.
`le_of_strongLT` theorem le_of_strongLT : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → Preorder (π i)] {a b : (i : ι) → π i}, StrongLT a b → a ≤ b This theorem, `le_of_strongLT`, states that for any type `ι` and for any type mapping `π : ι → Type`, given a preorder relation (a binary relation that is reflexive and transitive) on each `π i`, for any two functions `a` and `b` of type `(i : ι) → π i`, if `a` is strongly less than `b` (meaning the value of `a i` is strictly less than `b i` for every `i`), then `a` is also less than or equal to `b`. More concisely: If `π : ι → Type` is a type mapping and `≤_π : ∀ i, π i → π i → Prop` is a preorder on each `π i`, and `a, b : ι → π i` are functions such that `a i < b i` for all `i`, then `a i ≤ b i` for all `i`.
`Eq.trans_lt` theorem Eq.trans_lt : ∀ {α : Type u} {a b c : α} [inst : LT α], a = b → b < c → a < c This theorem, named "Eq.trans_lt", states that for any type `α` with a less-than relationship (`LT`), if an element `a` is equal to an element `b` (`a = b`), and `b` is less than another element `c` (`b < c`), then `a` is less than `c` (`a < c`). Essentially, it transmits the less-than relationship through an equality: equality and a 'less-than' relationship together imply another 'less-than' relationship. More concisely: If `a = b` and `b < c`, then `a < c`.
`ltByCases_gt` theorem ltByCases_gt : ∀ {α : Type u} [inst : LinearOrder α] {P : Sort u_3} {x y : α} (h : y < x) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P}, ltByCases x y h₁ h₂ h₃ = h₃ h The theorem `ltByCases_gt` states that for any type `α` which has a linear order, for any propositions `P`, and for any values `x` and `y` of type `α`, given a proof `h` that `y < x`, and three proof objects `h₁`, `h₂`, and `h₃` corresponding to cases where `x < y`, `x = y`, and `y < x` respectively, the function `ltByCases x y h₁ h₂ h₃` will return `h₃ h`. In other words, when `y < x`, the function `ltByCases` correctly chooses the proof object `h₃` associated with this case. More concisely: For any type `α` with a linear order, given `x`, `y` in `α` and proofs `h: y < x`, `h₁: x < y`, `h₂: x = y`, the function `ltByCases x y h₁ h₂ h₃` returns `h₃` when `x < y`.
`LE.le.lt_iff_ne` theorem LE.le.lt_iff_ne : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → (a < b ↔ a ≠ b) This theorem states that for all types `α` with a partial order, given two elements `a` and `b` of that type, if `a` is less than or equal to `b`, then `a` is strictly less than `b` if and only if `a` is not equal to `b`. That is, in a partially ordered set, if `a` isn't equal to `b`, then it must be strictly less than `b` given that `a` is already less than or equal to `b`. More concisely: In a partially ordered set, `a` is strictly less than `b` if and only if `a` is less than `b` and `a` is not equal to `b`.
`Preorder.toLE_injective` theorem Preorder.toLE_injective : ∀ {α : Type u_3}, Function.Injective (@Preorder.toLE α) This theorem states that for any type `α`, the function `Preorder.toLE` is injective. In other words, if we have two preorders on `α` such that the "less than or equal to" relation derived from them, `Preorder.toLE`, is the same for both, then the two preorders must be the same. So, no two distinct preorders can give rise to the same "less than or equal to" relation. More concisely: If two preorders on a type `α` have equal "less than or equal to" relations `Preorder.toLE`, then they are equal.
`LE.ext` theorem LE.ext : ∀ {α : Type u} (x y : LE α), LE.le = LE.le → x = y This theorem states that for any type `α`, if we have two instances `x` and `y` of the less-or-equal relation (`LE`) on `α`, and if their less-equal functions (marked by `LE.le`) are the same, then `x` and `y` must also be the same. Essentially, it asserts that the less-equal relation on a certain type is uniquely determined by its less-equal function. More concisely: For any type `α` and instances `x` and `y` of the less-or-equal relation on `α` with equal less-equal functions `LE.le`, we have `x = y`.
`not_le_of_lt` theorem not_le_of_lt : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a This theorem states that for any type `α` that has a preorder, if `a` is less than `b` then `b` cannot be less than or equal to `a`. In more mathematical terms, for all `a` and `b` in a preordered set, if `a < b` then it's not the case that `b ≤ a`. This is a property of the ordering relation in a preorder, which is a mathematical structure where the relation is reflexive and transitive. More concisely: In a preorder, for all `a` and `b`, if `a` is strictly less than `b`, then `b` is not less than or equal to `a`.
`Eq.ge` theorem Eq.ge : ∀ {α : Type u} [inst : Preorder α] {x y : α}, x = y → y ≤ x This theorem, `Eq.ge`, states that for any given type `α` that has a preorder relationship, if `x` is equal to `y` then `y` is less than or equal to `x`. Preorder is a binary relation that is reflexive and transitive. It's important to note that in the Lean mathlib, the `≤` (is less than or equal to) operator is used almost exclusively, hence `y ≤ x` is used here instead of `x ≥ y` (is greater than or equal to). More concisely: For all types `α` with a preorder relation and all `x y` of type `α`, if `x = y`, then `y ≤ x`.
`lt_iff_lt_of_le_iff_le'` theorem lt_iff_lt_of_le_iff_le' : ∀ {α : Type u} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} {c d : β}, (a ≤ b ↔ c ≤ d) → (b ≤ a ↔ d ≤ c) → (b < a ↔ d < c) This theorem states that for all types `α` and `β` with a preorder relation, given any elements `a`, `b` from `α` and `c`, `d` from `β`, if the implication that `a` is less than or equal to `b` if and only if `c` is less than or equal to `d` holds, and also the implication that `b` is less than or equal to `a` if and only if `d` is less than or equal to `c` holds, then the theorem guarantees that the implication that `b` is strictly less than `a` holds if and only if `d` is strictly less than `c`. In simpler terms, this is about the equivalence of order relations in two preordered sets under certain conditions. More concisely: If `α` and `β` are preordered sets with equivalent order relations between `a ≤ b` in `α` and `c ≤ d` in `β`, and between `b ≤ a` in `α` and `d ≤ c` in `β`, then `b < a` in `α` if and only if `d < c` in `β`.
`Eq.le` theorem Eq.le : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a = b → a ≤ b This theorem, known as `Eq.le`, states that for any preordered type `α` and any two elements `a` and `b` of that type, if `a` is equal to `b`, then `a` is less than or equal to `b`. In other words, in any preordered set, an element is always less than or equal to itself. More concisely: In any preordered type, for all elements `a` and `b`, if `a = b`, then `a ≤ b`.
`LE.le.trans` theorem LE.le.trans : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c This theorem, named `LE.le.trans` in Lean 4, states that the "less than or equal to" (`≤`) relation is transitive on a preorder. In more detail, given a preorder of some type `α` and three elements `a`, `b`, and `c` of that type, if `a` is less than or equal to `b` and `b` is less than or equal to `c`, then `a` is less than or equal to `c`. This theorem is an alias of `le_trans`, meaning it's another name for the same concept or proof. More concisely: If `a ≤ b` and `b ≤ c`, then `a ≤ c`. (In the context of a preorder.)
`Subtype.coe_lt_coe` theorem Subtype.coe_lt_coe : ∀ {α : Type u} [inst : LT α] {p : α → Prop} {x y : Subtype p}, ↑x < ↑y ↔ x < y This theorem states that for any type `α` that has a less-than (`<`) operation, and for any property `p` that applies to `α`, then for any two subtypes `x` and `y` of `α` satisfying property `p`, `x` is less than `y` if and only if the underlying value of `x` (obtained using the coercion function `↑x`) is less than the underlying value of `y` (`↑y`). In simpler terms, it means that the order relation `<` is preserved when transitioning from subtype to its underlying value. More concisely: For any type `α` with a `<` operation and any subtypes `x` and `y` of `α` satisfying a property `p`, if `x < y` then `↑x < ↑y`.
`LT.lt.trans_le` theorem LT.lt.trans_le : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, a < b → b ≤ c → a < c This theorem, `LT.lt.trans_le`, is an alias of `lt_of_lt_of_le`. It states that for any type `α` which has a `Preorder` instance, if `a`, `b` and `c` are elements of `α`, and if `a` is less than `b` and `b` is less than or equal to `c`, then `a` is less than `c`. This theorem generalizes the concept of transitivity of the less-than relation to the less-than-or-equal-to relation. More concisely: If `α` is a preordered type and `a`, `b`, `c` are elements of `α` with `a < b` and `b <= c`, then `a < c`.
`LE.le.le_iff_eq` theorem LE.le.le_iff_eq : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → (b ≤ a ↔ b = a) This theorem states that for any given type `α` with a partial order, and for any two elements `a` and `b` of this type such that `a` is less than or equal to `b`, then `b` is less than or equal to `a` if and only if `b` is equal to `a`. Essentially, in a partial order, when `a` is not strictly greater than `b`, the only way for `b` to be not strictly greater than `a` is for `b` and `a` to be equal. More concisely: In a partial order, for all types `α` and elements `a` and `b` of `α`, if `a` is less than or equal to `b` and `b` is not strictly greater than `a`, then `a` and `b` are equal.
`exists_forall_ge_and` theorem exists_forall_ge_and : ∀ {α : Type u} [inst : LinearOrder α] {p q : α → Prop}, (∃ i, ∀ j ≥ i, p j) → (∃ i, ∀ j ≥ i, q j) → ∃ i, ∀ j ≥ i, p j ∧ q j This theorem states that for any type `α` that is a linear order, given two properties `p` and `q` that each element of `α` might satisfy, if there exists an element `i` such that for all elements `j` greater than or equal to `i`, `p` holds, and similarly for `q`, then there exists an element `i` such that for all elements `j` greater than or equal to `i`, both `p` and `q` hold. In other words, if we can find a point in the order after which all elements satisfy `p` and a point after which all elements satisfy `q`, we can find a point after which all elements satisfy both `p` and `q`. More concisely: If `α` is a linear order and there exist elements `i` such that for all `j ≥ i`, both `p(j)` and `q(j)` hold, then there exists an element `i' ≤ i` such that for all `j ≥ i'`, both `p(j)` and `q(j)` hold.
`ltByCases_lt` theorem ltByCases_lt : ∀ {α : Type u} [inst : LinearOrder α] {P : Sort u_3} {x y : α} (h : x < y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P}, ltByCases x y h₁ h₂ h₃ = h₁ h This theorem, `ltByCases_lt`, states that for any type `α` equipped with a decidable linear order, any two elements `x` and `y` of that type, and any property `P`, if `x < y`, then the result of the function `ltByCases` applied to `x`, `y` and three functions `h₁`, `h₂` and `h₃` (which map from the conditions `x < y`, `x = y`, `y < x` to `P` respectively) is equal to the result of `h₁` applied to the condition `x < y`. In other words, when `x < y`, `ltByCases` correctly chooses the function `h₁` that handles the case `x < y`. More concisely: For any decidably ordered type `α` and elements `x` and `y` of `α`, if `x < y`, then `ltByCases(x, y, h₁, h₂, h₃) = h₁ (x < y)`.
`LT.lt.trans_eq'` theorem LT.lt.trans_eq' : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, b < c → a = b → a < c This theorem, `LT.lt.trans_eq'`, states that for any given type `α` with a defined preorder, if `b` is less than `c` and `a` equals `b`, then `a` is less than `c`. In other words, it allows us to transitively infer the inequality relationship from `a` to `c` via the equality relationship between `a` and `b` and the inequality relationship between `b` and `c`. More concisely: If `a` is equal to `b` and `b` is less than `c` in a preordered type `α`, then `a` is less than `c`.
`ge_of_eq` theorem ge_of_eq : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a = b → a ≥ b This theorem states that for any type `α` with a preorder structure (a set equipped with a reflexive and transitive binary relation), and for any two elements `a` and `b` of type `α`, if `a` is equal to `b` then `a` is greater than or equal to `b`. This is an intuitive result given the reflexivity of preorders, which states that every element should be at least 'as big as' itself. More concisely: In a preorder, if `a` is related (equivalent) to `b`, then `a` is greater than or equal to `b`.
`max_def'` theorem max_def' : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), max a b = if b ≤ a then a else b This theorem states that for any type `α` that has a linear order, the maximum of two elements `a` and `b` of this type is defined as follows: If `b` is less than or equal to `a`, then `a` is the maximum; otherwise, `b` is the maximum. Essentially, it's a formal way of saying the maximum of `a` and `b` is `a` if `a` is greater than or equal to `b`, and `b` otherwise. More concisely: For any type `α` with a linear order, the maximum of `a` and `b` is `a` if `a` is greater than or equal to `b`, and `b` otherwise.
`eq_iff_le_not_lt` theorem eq_iff_le_not_lt : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a = b ↔ a ≤ b ∧ ¬a < b This theorem states that for any two elements `a` and `b` of a type `α` that has a partial order, `a` is equal to `b` if and only if `a` is less than or equal to `b` and it is not the case that `a` is less than `b`. This essentially captures the notion of equality in a partial order, where `a` and `b` being equal means that neither is strictly greater than the other, but they can be equal or less than each other. More concisely: In a partial order, two elements are equal if and only if they are comparable and neither is strictly less than the other.
`LE.le.trans'` theorem LE.le.trans' : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, b ≤ c → a ≤ b → a ≤ c This theorem, often referred to as an "alias" of `le_trans'`, is a property that states the transitivity of the less than or equal to (≤) relation over a preordered set. In more concrete terms, for any type `α` with a preorder structure, and any three elements `a`, `b`, and `c` of this type, if `b` is less than or equal to `c` and `a` is less than or equal to `b`, then it follows that `a` is less than or equal to `c`. This rule is fundamental in the theory of ordered sets. More concisely: For any preordered type `α` and elements `a`, `b`, and `c` in `α`, if `b ≤ c` and `a ≤ b`, then `a ≤ c`.
`max_rec'` theorem max_rec' : ∀ {α : Type u} [inst : LinearOrder α] {x y : α} (p : α → Prop), p x → p y → p (max x y) This theorem, `max_rec'`, is a universal property of the maximum of two elements in a linearly ordered type. It states that for any type `α` whose elements are linearly ordered and for any two elements `x` and `y` of that type, if a property `p` holds for both `x` and `y`, then the same property `p` also holds for the maximum of `x` and `y`. In other words, if `p` is true for `x` and `y`, then `p` is true for `max x y`. More concisely: For all linearly ordered types `α` and elements `x` and `y` of `α`, if a property `p` holds for both `x` and `y`, then `p` holds for their maximum `max x y`.
`eq_of_le_of_forall_le_of_dense` theorem eq_of_le_of_forall_le_of_dense : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] {a₁ a₂ : α}, a₂ ≤ a₁ → (∀ (a : α), a₂ < a → a₁ ≤ a) → a₁ = a₂ This theorem states that for all types `α` that have a linear order and are densely ordered, if we have two elements `a₁` and `a₂` of this type such that `a₂` is less than or equal to `a₁`, and for every element `a` of type `α`, if `a₂` is less than `a`, then `a₁` is less than or equal to `a`, then `a₁` must be equal to `a₂`. Essentially, it proves that in a densely ordered set, if one element is less than or equal to another and this remains true no matter how close we get to the second element from above, the two elements must be equal. More concisely: In a densely ordered type `α`, if `a₁ ≤ a₂` and for all `a ∈ α` with `a₂ < a`, we have `a₁ ≤ a`, then `a₁ = a₂`.
`LE.le.trans_lt'` theorem LE.le.trans_lt' : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, b ≤ c → a < b → a < c This theorem, `LE.le.trans_lt'`, states that for any given type `α` that has a preorder structure, if we have three elements `a`, `b`, and `c` of this type such that `b` is less than or equal to `c` (`b ≤ c`) and `a` is strictly less than `b` (`a < b`), then `a` is strictly less than `c` (`a < c`). In essence, it is a statement about the transitivity of the "less than" relation in the context of preordered sets. More concisely: If `a < b` and `b ≤ c` in a preordered type `α`, then `a < c`.
`LT.lt.not_le` theorem LT.lt.not_le : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a This theorem, `LT.lt.not_le`, states that for any type `α` with a `Preorder` instance and any two elements `a` and `b` of that type, if `a` is strictly less than `b` (`a < b`), then it is not the case that `b` is less than or equal to `a` (`¬b ≤ a`). This is a fundamental property in order theory which holds for all preordered sets, and serves as an alias of the `not_le_of_lt` theorem. More concisely: For any preordered type `α` and elements `a` and `b` of type `α`, if `a` is strictly less than `b`, then `b` is not less than or equal to `a`.
`LE.le.eq_of_not_gt` theorem LE.le.eq_of_not_gt : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → ¬a < b → b = a This theorem, named `LE.le.eq_of_not_gt`, states that for any type `α` with a partial order, if `a` and `b` are two elements of this type where `a` is less than or equal to `b` and `a` is not less than `b`, then `b` must be equal to `a`. Essentially, it gives us a way to establish equality between two elements in a partially ordered set based on ordering conditions. More concisely: If `α` is a type with a partial order, and `a` and `b` are elements of `α` with `a ≤ b` and `a < b` being false, then `a = b`.
`exists_between` theorem exists_between : ∀ {α : Type u} [inst : LT α] [inst_1 : DenselyOrdered α] {a₁ a₂ : α}, a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂ This theorem, named `exists_between`, states that for any type `α` that has a less-than relation and is densely ordered, given two elements `a₁` and `a₂` of type `α`, if `a₁` is less than `a₂`, then there exists another element `a` in type `α` which lies between `a₁` and `a₂`. In other words, in any densely ordered set, between any two distinct elements, there always exists another element. More concisely: In any densely ordered type, for all distinct elements `a₁` and `a₂`, there exists an element `a` such that `a₁` < `a` < `a₂`.
`StrongLT.trans_le` theorem StrongLT.trans_le : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → Preorder (π i)] {a b c : (i : ι) → π i}, StrongLT a b → b ≤ c → StrongLT a c The theorem `StrongLT.trans_le` states that for any index type `ι`, any function `π` from `ι` to a type with a preorder, and for any three such functions `a`, `b`, and `c`, if `a` is strongly less than `b`, and `b` is less than or equal to `c` (for all indices), then `a` is strongly less than `c`. In other words, this theorem implements a form of transitivity for the `StrongLT` relation in the presence of a `Preorder`. In the context of this theorem, `StrongLT a b` means that for each index `i`, `a i` is strictly less than `b i`, and `b ≤ c` means that for each index `i`, `b i` is less than or equal to `c i`. More concisely: For any index type `ι`, given functions `π : ι → (type with preorder)` and `a, b, c : π ι`, if `a StrongLT b` and `b ≤ c`, then `a StrongLT c` holds in the preorder.
`LT.lt.trans'` theorem LT.lt.trans' : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, b < c → a < b → a < c This theorem, referred to as an alias of `lt_trans'`, states that for any type `α` with a preorder structure, if an element `b` is less than an element `c` and an element `a` is less than `b`, then `a` is less than `c`. In other words, it's establishing the concept of transitivity for the less-than relation in the context of preordered sets. More concisely: If `α` is a preordered type and `a` < `b` < `c`, then `a` < `c`.
`ge_antisymm` theorem ge_antisymm : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → b = a The theorem `ge_antisymm` states that for any type `α` that has a partial order, and any two elements `a` and `b` of that type, if `a` is less than or equal to `b`, and `b` is less than or equal to `a`, then `b` must be equal to `a`. This is a formalization of the antisymmetry property of partial orders. More concisely: For any type with a partial order, if `a` is less than or equal to `b` and `b` is less than or equal to `a`, then `a` and `b` are equal.
`lt_self_iff_false` theorem lt_self_iff_false : ∀ {α : Type u} [inst : Preorder α] (x : α), x < x ↔ False This theorem, `lt_self_iff_false`, states that for any type, `α`, equipped with a preorder relation, an element `x` of type `α` cannot be strictly less than itself. In other words, `x < x` is always false. The principle of this theorem reflects the antisymmetry of preorders in mathematics, where an element cannot be both less than and greater than another element, especially itself. More concisely: For any type `α` with a preorder relation, `x < x` is always false.
`LE.le.eq_or_gt` theorem LE.le.eq_or_gt : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → b = a ∨ a < b This theorem, named `LE.le.eq_or_gt`, is an alias of the theorem `eq_or_gt_of_le`. It applies to any type `α` that has a `PartialOrder` relation. The theorem takes two elements `a` and `b` of this type and a proof that `a` is less than or equal to `b`. It then states that either `b` is equal to `a`, or `a` is strictly less than `b`. This is a fundamental property in order theory, asserting that for any two elements in a partially ordered set, if one element is not greater than the other, then either they are equal or the first is strictly less than the second. More concisely: If `a` is less than or equal to `b` in a partially ordered set, then either `a` is equal to `b` or `a` is strictly less than `b`.
`PartialOrder.ext` theorem PartialOrder.ext : ∀ {α : Type u_3} {A B : PartialOrder α}, (∀ (x y : α), x ≤ y ↔ x ≤ y) → A = B This theorem states that for any given type `α`, if two `PartialOrder` structures `A` and `B` on `α` have the property that, for every pair of elements `x` and `y` in `α`, `x` is less than or equal to `y` in `A` if and only if `x` is less than or equal to `y` in `B`, then `A` and `B` must be the same PartialOrder structure. In other words, two partial order structures on the same type are equal if they induce the same ordering on pairs of elements. More concisely: If two PartialOrder structures on the same type induce the same relation between pairs of elements, then they are equal.
`not_lt_of_le` theorem not_lt_of_le : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a ≤ b → ¬b < a This theorem states that for any type `α` that has a `Preorder` instance, and for any two elements `a` and `b` of this type, if `a` is less than or equal to `b`, then `b` is not less than `a`. In terms of mathematical language, this theorem asserts that for all `a` and `b` in a preordered set, if `a` ≤ `b`, then it is not the case that `b` < `a`. More concisely: In a preordered set, if `a` is less than or equal to `b`, then `b` is not strictly less than `a`.
`LE.le.trans_lt` theorem LE.le.trans_lt : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < c This theorem, called `LE.le.trans_lt`, is an alias of `lt_of_le_of_lt`. It states that for any type `α` which has a predefined ordering (`Preorder`), if you have three elements `a`, `b`, and `c` of this type such that `a` is less than or equal to `b` and `b` is strictly less than `c`, you can conclude that `a` is strictly less than `c`. This theorem allows for the transitive property of inequalities in a preorder to be applied in cases where there is a combination of non-strict and strict inequalities. More concisely: If `a` is less than or equal to `b` and `b` is strictly less than `c` in a preordered type `α`, then `a` is strictly less than `c`.
`GT.gt.lt` theorem GT.gt.lt : ∀ {α : Type u} [inst : LT α] {x y : α}, x > y → y < x This theorem states that for any type `α` that has a less-than operation (`LT α`), given any two elements `x` and `y` of type `α`, if `x` is greater than `y` (`x > y`), then `y` is less than `x` (`y < x`). It essentially describes the basic property of ordered sets where the greater-than and less-than relations are inverse of each other. More concisely: For any type `α` with a total order (`LT α`), the relation `x > y` implies `y < x`.
`eq_or_eq_or_eq_of_forall_not_lt_lt` theorem eq_or_eq_or_eq_of_forall_not_lt_lt : ∀ {α : Type u} [inst : LinearOrder α], (∀ ⦃x y z : α⦄, x < y → y < z → False) → ∀ (x y z : α), x = y ∨ y = z ∨ x = z This theorem states that if a linearly ordered set does not contain any set of three elements `x`, `y`, and `z` such that `x < y < z`, then any three elements `x`, `y`, and `z` from this set must either be the same or two of them must be identical. In other words, in such a set, any three elements are either all the same, or one of them is equal to one of the others. More concisely: In a linearly ordered set, the absence of a triple `(x, y, z)` with `x < y < z` implies that any three elements are equal or two of them are identical.
`LT.lt.ne` theorem LT.lt.ne : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → a ≠ b This theorem, `LT.lt.ne`, is an alias of `ne_of_lt`. For any given type `α` that has a `Preorder` instance (meaning that you can compare two elements of the type through "less than" or "greater than"), it states that if `a` and `b` are elements of `α` and `a` is less than `b` (`a < b`), then `a` is not equal to `b` (`a ≠ b`). In other words, this theorem formalizes the intuitive concept that a number is not equal to another number that is greater than it. More concisely: For all types `α` with a `Preorder` instance, `a < b` implies `a ≠ b`.
`LE.le.trans_eq'` theorem LE.le.trans_eq' : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, b ≤ c → a = b → a ≤ c This theorem, `LE.le.trans_eq'`, states that for any type `α` with a preorder structure and any three elements `a`, `b`, and `c` of that type, if `b` is less than or equal to `c` and `a` is equal to `b`, then `a` is less than or equal to `c`. This is essentially an alternative formulation of the transitive property of inequality, allowing substitution of equal elements, in the context of a particular preorder. More concisely: If `α` is a preordered type, `a`, `b`, and `c` are elements of `α`, and `b` is less than or equal to `c` and `a` equals `b`, then `a` is less than or equal to `c`.
`Pi.lt_def` theorem Pi.lt_def : ∀ {ι : Type u} {α : ι → Type v} [inst : (i : ι) → Preorder (α i)] {x y : (i : ι) → α i}, x < y ↔ x ≤ y ∧ ∃ i, x i < y i The theorem `Pi.lt_def` states that for any type `ι` and any type map `α : ι → Type v`, given a Preorder on each type `α i`, for any two functions `x, y : (i : ι) → α i`, `x` is less than `y` if and only if `x` is less than or equal to `y` and there exists some `i` such that `x i` is strictly less than `y i`. This theorem essentially provides a definition for the "less than" relation in the context of these function spaces. More concisely: For any preordered type ι and type map α : ι → Type, the function space α → α has a "less than" relation defined as reflexive, transitive, and such that x < y if and only if x ≤ y and ∃ i, x i < y i.
`Ne.lt_of_le` theorem Ne.lt_of_le : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≠ b → a ≤ b → a < b This theorem states that for any type `α` that has a partial order, if we have two elements `a` and `b` of type `α`, then `a` is strictly less than `b` (`a < b`) if `a` is not equal to `b` (`a ≠ b`) and `a` is less than or equal to `b` (`a ≤ b`). More concisely: For any type `α` with a partial order, `a < b` if and only if `a ≠ b` and `a ≤ b`.
`eq_of_forall_le_iff` theorem eq_of_forall_le_iff : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, (∀ (c : α), c ≤ a ↔ c ≤ b) → a = b := by sorry This theorem, `eq_of_forall_le_iff`, states that for any type `α` that has a partial order, given any two elements `a` and `b` of type `α`, if for every other element `c` of `α`, `c` is less than or equal to `a` if and only if `c` is less than or equal to `b`, then `a` must be equal to `b`. In other words, if `a` and `b` have the same order relationship with all other elements in the set, they are equal. More concisely: If two elements `a` and `b` in a partially ordered type `α` have the same relation to all other elements, then `a` and `b` are equal.
`LT.lt.trans` theorem LT.lt.trans : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, a < b → b < c → a < c This theorem, which is an alias of `lt_trans`, states that for any type `α` that has a `Preorder` structure, if `a`, `b`, `c` are objects of `α` and `a` is less than `b`, and `b` is less than `c`, then `a` is less than `c`. This is essentially transitivity of the less than relation in a preordered set. More concisely: In a preordered set, if `a` is less than `b` and `b` is less than `c`, then `a` is less than `c`.
`LE.le.eq_of_not_lt` theorem LE.le.eq_of_not_lt : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → ¬a < b → a = b This theorem, `LE.le.eq_of_not_lt`, states that for any type `α` that has a partial order, if `a` and `b` are elements of `α` such that `a` is less than or equal to `b`, and it is not the case that `a` is strictly less than `b`, then `a` must be equal to `b`. This is in fact just an alias of the theorem `eq_of_le_of_not_lt` in Lean. More concisely: If `α` is a partially ordered type and `a` and `b` are elements of `α` with `a ≤ b` and `a < b` being false, then `a = b`.
`LE.le.antisymm` theorem LE.le.antisymm : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b This theorem, which is an alias of `le_antisymm`, states that for any partially ordered set `α`, if an element `a` is less than or equal to another element `b`, and `b` is also less than or equal to `a`, then `a` and `b` are actually equal. This is a fundamental property of partial orders, reflecting the antisymmetry characteristic of such structures. More concisely: In a partially ordered set, if x <= y and y <= x, then x = y.
`Mathlib.Order.Basic._auxLemma.2` theorem Mathlib.Order.Basic._auxLemma.2 : ∀ {α : Type u} [inst : Preorder α] (x : α), (x < x) = False This theorem, `Mathlib.Order.Basic._auxLemma.2`, states that for any type `α` where a preorder is defined, for any element `x` of that type, the proposition that `x` is less than itself is false. In other words, it establishes the irreflexivity of the "less than" relation in a preorder, i.e., no element in the set can be less than itself. More concisely: In any preorder, no element is less than itself.
`LE.le.eq_or_lt` theorem LE.le.eq_or_lt : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → a = b ∨ a < b This theorem, named `LE.le.eq_or_lt`, states that for any given type `α` that has a partial order, and any two elements `a` and `b` of that type, if `a` is less than or equal to `b`, then either `a` is equal to `b` or `a` is strictly less than `b`. This is just an alias of the theorem `eq_or_lt_of_le`. More concisely: For any type with a partial order, if `a` is less than or equal to `b`, then `a` is equal to `b` or `a` is strictly less than `b`.
`Function.const_le_const` theorem Function.const_le_const : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Nonempty β] {a b : α}, Function.const β a ≤ Function.const β b ↔ a ≤ b The theorem `Function.const_le_const` states that, for all types `α` and `β`, where `α` has a preorder and `β` is nonempty, and for all elements `a` and `b` of `α`, the constant function with value `a` for the type `β` is less than or equal to the constant function with value `b` for the same type `β` if and only if `a` is less than or equal to `b`. It essentially relates the order of the values of two constant functions to the order of their function values. More concisely: For all types with a preorder, and for all constants `a` and `b` of such a type, the constant functions with values `a` and `b` are equal if and only if `a` is less than or equal to `b`. (Note: The given Lean theorem statement states that the constant functions are related by the preorder, but the mathematical statement more directly states that the constants themselves are related by the preorder relation.)
`lt_or_lt_iff_ne` theorem lt_or_lt_iff_ne : ∀ {α : Type u} [inst : LinearOrder α] {x y : α}, x < y ∨ y < x ↔ x ≠ y This theorem, `lt_or_lt_iff_ne`, states that for any type `α` that has a linear order, and for any two elements `x` and `y` of this type, the assertion that `x` is less than `y` or `y` is less than `x` is equivalent to `x` not being equal to `y`. This theorem essentially captures the fact that in a linear order, two elements are unequal if and only if one of them is strictly less than the other. More concisely: In a linear order, `x` is less than `y` or `y` is less than `x` if and only if `x` is not equal to `y`.
`LE.le.gt_iff_ne` theorem LE.le.gt_iff_ne : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → (a < b ↔ b ≠ a) This theorem states that for any type `α` that has a partial order, for any two elements `a` and `b` of type `α`, if `a` is less than or equal to `b`, then `a` is strictly less than `b` if and only if `b` is not equal to `a`. In other words, the only way `a` can be strictly less than `b` is if `a` and `b` are not the same element, given that `a` is less than or equal to `b`. This is a basic property of ordered sets. More concisely: In an ordered set, for all elements `a` and `b`, if `a ≤ b` then `a < b` if and only if `a ≠ b`.
`LT.lt.false` theorem LT.lt.false : ∀ {α : Type u} [inst : Preorder α] {x : α}, x < x → False The theorem `LT.lt.false` states that for any type `α` which has a preorder relation, and for any element `x` of type `α`, the statement that `x` is less than itself is always false. This corresponds to the antisymmetry property of preorder relations, which asserts that no element can be strictly less than itself. More concisely: For any preordered type `α` and its element `x`, `x` is not less than `x`.
`Mathlib.Order.Basic._auxLemma.25` theorem Mathlib.Order.Basic._auxLemma.25 : ∀ {α : Type u} [inst : LE α] {p : α → Prop} {x y : α} {hx : p x} {hy : p y}, (⟨x, hx⟩ ≤ ⟨y, hy⟩) = (x ≤ y) := by sorry This theorem, `Mathlib.Order.Basic._auxLemma.25`, states that for any type `α` with a less than or equal to (`≤`) ordering and a property `p` acting on elements of `α`, and given two elements `x` and `y` of `α` for which `p` holds (that is, `p x` and `p y` are true), then the inequality of the pairs `{ val := x, property := hx }` and `{ val := y, property := hy }` (where `hx` and `hy` denote the truth of `p` for `x` and `y` respectively) is equivalent to the inequality `x ≤ y`. In essence, it asserts that the order of the pairs is determined solely by the order of their value components. More concisely: For any type `α` with a total ordering and property `p`, if `x ≤ y` and `p x` hold, then `{x, p x} ≤ {y, p y}`.
`le_of_forall_lt'` theorem le_of_forall_lt' : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, (∀ (c : α), a < c → b < c) → b ≤ a := by sorry This theorem, `le_of_forall_lt'`, states that for any type `α` that has a linear order, if for every element `c` of `α` the condition "if `a` is less than `c` then `b` is less than `c`" holds true, then `b` is less than or equal to `a`. This provides a way to establish an inequality relation between two elements in a linearly ordered set based on their relation to all other elements in the set. Essentially, if `b` is always less than any number that `a` is less than, then `b` must be less than or equal to `a`. More concisely: If every element less than `a` in a linearly ordered set is less than `b`, then `b` is less than or equal to `a`.
`LE.le.lt_of_ne'` theorem LE.le.lt_of_ne' : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≠ a → a < b This theorem, known as an alias of `lt_of_le_of_ne'`, states that for any type `α` that has a partial order, if `a` and `b` are elements of `α` such that `a` is less than or equal to `b` and `b` is not equal to `a`, then `a` is less than `b`. It's a fundamental result in order theory that helps express the relationship between less-than and less-than-or-equal-to under the condition of non-equality. More concisely: If `α` is a partially ordered type and `a` and `b` are elements of `α` with `a ≤ b` and `a ≠ b`, then `a < b`.
`Mathlib.Order.Basic._auxLemma.10` theorem Mathlib.Order.Basic._auxLemma.10 : ∀ {α : Type u} [inst : Preorder α] {a b : α}, (a < b) = (a ≤ b ∧ ¬b ≤ a) This theorem states that for any type `α` equipped with a preorder, and for any two elements `a` and `b` of this type, `a` is less than `b` if and only if `a` is less than or equal to `b` and it is not the case that `b` is less than or equal to `a`. More concisely: For any preordered type `α`, elements `a` and `b` satisfy `a < b` if and only if `a ≤ b` and not `b ≤ a`.
`LE.le.lt_of_ne` theorem LE.le.lt_of_ne : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → a ≠ b → a < b This theorem, `LE.le.lt_of_ne`, states that for any type `α` that has a partial order, given two elements `a` and `b` of type `α`, if `a` is less than or equal to `b` and `a` is not equal to `b`, then `a` is strictly less than `b`. This is essentially a restatement of the `lt_of_le_of_ne` theorem, acting as an alias for convenience. More concisely: If `α` is a type with a partial order, and `a` and `b` are elements of `α` with `a ≤ b` and `a ≠ b`, then `a < b`.
`LE.le.antisymm'` theorem LE.le.antisymm' : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → b = a This theorem, named `LE.le.antisymm'`, is essentially an alias of `ge_antisymm`. It states that for any type `α` that has a `PartialOrder` structure, if one element `a` is less than or equal to another element `b`, and `b` is also less than or equal to `a`, then `b` and `a` are equal. This is a fundamental property of partially ordered sets, reflecting the antisymmetry characteristic of these structures. More concisely: In a partially ordered set, if `a` is less than or equal to `b` and `b` is less than or equal to `a`, then `a` and `b` are equal.
`le_of_forall_le_of_dense` theorem le_of_forall_le_of_dense : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] {a₁ a₂ : α}, (∀ (a : α), a₂ < a → a₁ ≤ a) → a₁ ≤ a₂ This theorem states that for any type `α` that has a linear order and is densely ordered, if for every element `a` such that `a₂` is less than `a`, `a₁` is less than or equal to `a`, then `a₁` is less than or equal to `a₂`. In other words, if `a₁` is less than or equal to any element that's larger than `a₂`, then `a₁` must be less than or equal to `a₂`. This applies to any type that fulfills the conditions of being linearly ordered and densely ordered, like the real numbers. More concisely: If a type `α` is linearly and densely ordered, then for all `a₁` and `a₂` in `α` with `a₂` > `a₁`, if `a₁` ≤ `x` for all `x` with `a₁` < `x` < `a₂`, then `a₁` ≤ `a₂`.
`LT.lt.trans_le'` theorem LT.lt.trans_le' : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, b < c → a ≤ b → a < c This theorem, `LT.lt.trans_le'`, is actually an alias of `lt_of_lt_of_le'`. It states that for any type `α` that has a preorder relation, given three elements `a`, `b`, and `c` of that type, if `b` is less than `c` (`b < c`) and `a` is less than or equal to `b` (`a ≤ b`), then it can be concluded that `a` is less than `c` (`a < c`). This theorem is a form of transitivity property for less than relation in a preordered set. More concisely: If `a <= b` and `b < c` hold in a preordered type `α`, then `a < c` also holds.
`Eq.trans_ge` theorem Eq.trans_ge : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, b = c → a ≤ b → a ≤ c This theorem, `Eq.trans_ge`, is an alias of `le_of_eq_of_le'` in Lean 4. It states that, for any preorder structure `α` and for any three elements `a`, `b`, and `c` of this structure, if `b` is equal to `c` (`b = c`) and `a` is less than or equal to `b` (`a ≤ b`), then `a` is also less than or equal to `c` (`a ≤ c`). This theorem essentially allows us to substitute `b` with `c` in the inequality `a ≤ b` when `b = c`. More concisely: If `a` is less than or equal to `b` and `b` equals `c`, then `a` is less than or equal to `c`.
`LE.le.lt_of_not_le` theorem LE.le.lt_of_not_le : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a ≤ b → ¬b ≤ a → a < b This theorem, which is an alias of `lt_of_le_not_le`, states that for any type `α` with a preorder structure, if `a` and `b` are elements of type `α`, `a` is less than `b` if and only if `a` is less than or equal to `b` and it is not the case that `b` is less than or equal to `a`. In other words, in a preorder, `a` is strictly less than `b` if `a` is at most `b` but `b` is not at most `a`. More concisely: In a preorder, `a` is strictly less than `b` if and only if `a` is less than or equal to `b` and `b` is not less than or equal to `a`.
`commutative_of_le` theorem commutative_of_le : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] {f : β → β → α}, (∀ (a b : β), f a b ≤ f b a) → ∀ (a b : β), f a b = f b a This theorem states that to prove the commutativity of a binary operation `f`, where `f` is a function from type `β` to `α`, and `α` has a partial order defined, we only need to verify that `f(a, b)` is less than or equal to `f(b, a)` for all possible values of `a` and `b` of type `β`. If this condition is satisfied, then the theorem guarantees that `f(a, b)` is equal to `f(b, a)` for all `a` and `b`, i.e., the operation `f` is commutative. More concisely: If `f` is a function from type `β` to a partially ordered set `α`, then `f` is commutative if and only if `f(a, b) ≤ f(b, a)` for all `a, b` in `β`.
`Mathlib.Order.Basic._auxLemma.27` theorem Mathlib.Order.Basic._auxLemma.27 : ∀ {α : Type u} [inst : LE α] {p : α → Prop} {x y : Subtype p}, (↑x ≤ ↑y) = (x ≤ y) This theorem, `Mathlib.Order.Basic._auxLemma.27`, states that for any type `α` with a less than or equal to (`LE`) instance and a given property `p`, for any two subtypes `x` and `y` of `p`, the inequality between the underlying elements of `x` and `y` (`↑x ≤ ↑y`) is equivalent to the inequality between `x` and `y` themselves. In other words, the order of the elements when treated as subtypes is the same as the order of the elements in the original type. More concisely: For any type `α` with a `LE` instance and property `p`, the inequality `x ≤ y` between subtypes `x` and `y` of `p` is equivalent to `↑x ≤ ↑y` between their underlying elements.
`Mathlib.Order.Basic._auxLemma.29` theorem Mathlib.Order.Basic._auxLemma.29 : ∀ {α : Type u} {β : Type v} [inst : LE α] [inst_1 : LE β] {x₁ x₂ : α} {y₁ y₂ : β}, ((x₁, y₁) ≤ (x₂, y₂)) = (x₁ ≤ x₂ ∧ y₁ ≤ y₂) The theorem `Mathlib.Order.Basic._auxLemma.29` states that for any two types `α` and `β` that are partially ordered (i.e., have a "less than or equal to" (`≤`) relation defined on them), and for any pairs of elements `(x₁, y₁)` and `(x₂, y₂)` where `x₁`, `x₂` are from `α` and `y₁`, `y₂` are from `β`, the pair `(x₁, y₁)` is less than or equal to the pair `(x₂, y₂)` if and only if both `x₁` is less than or equal to `x₂` and `y₁` is less than or equal to `y₂`. This is an important property of how order relations extend to product types. More concisely: For any partially ordered types `α` and `β`, the order relation on their product `α × β` is given by `(x₁, y₁) ≤ (x₂, y₂)` if and only if `x₁ ≤ x₂` and `y₁ ≤ y₂`.
`LE.le.not_lt` theorem LE.le.not_lt : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a ≤ b → ¬b < a This theorem, also known as an alias of `not_lt_of_le`, states that for any type `α` that has a preorder, and for any two elements `a` and `b` of type `α`, if `a` is less than or equal to `b` then `b` is not less than `a`. In other words, if `a` is less than or equal to `b`, it is not possible for `b` to be less than `a` in the context of a preorder. More concisely: For any preorder (α, ≤), if a ≤ b then ∥ b < a \SyntaxError: unable to parse '∥ b < a' In Lean, use `not.lt` instead of `<` for the negation of the less-than relation in a preorder context: For any preorder (α, ≤), if a ≤ b then ∥ b < a \SyntaxError: unable to parse '∥ b < a' Correctly stated: For any preorder (α, ≤), if a ≤ b then ∀ (h : a ≤ b), ¬ (b < a) (using not.lt instead of <) So, the theorem statement can be concisely expressed as: In a preorder (α, ≤), if a ≤ b, then b cannot be less than a.
`LE.le.gt_or_eq` theorem LE.le.gt_or_eq : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → a < b ∨ b = a This theorem, known as "LE.le.gt_or_eq", states that for any type `α` which has a partial order, and any two instances `a` and `b` of that type, if `a` is less than or equal to `b`, then either `a` is strictly less than `b` or `b` is equal to `a`. This theorem serves as an alias for the `gt_or_eq_of_le` theorem. More concisely: For any type with a partial order, if `a` is less than or equal to `b`, then `a` is strictly less than `b` or `b` equals `a`.
`lt_iff_not_le` theorem lt_iff_not_le : ∀ {α : Type u} [inst : LinearOrder α] {x y : α}, x < y ↔ ¬y ≤ x This theorem, `lt_iff_not_le`, states that for any type of object `α` which has a linear ordering, for two objects `x` and `y` of this type, `x` is less than `y` if and only if it is not the case that `y` is less than or equal to `x`. This theorem essentially establishes the relationship between the "less than" (`<`) and "less than or equal to" (`≤`) operators in a linear order. More concisely: For any linear ordered type α, x and y in α, x < y if and only if y ≤ x does not hold.
`LE.le.lt_or_eq` theorem LE.le.lt_or_eq : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → a < b ∨ a = b This theorem, named `LE.le.lt_or_eq`, is essentially an alias of the theorem `lt_or_eq_of_le`. It applies to any type `α` that has a partial order. For any two elements `a` and `b` of this type, if `a` is less than or equal to `b`, then it must be the case that either `a` is strictly less than `b`, or `a` is equal to `b`. More concisely: For any type with a partial order, if `a` is less than or equal to `b`, then `a` is strictly less than `b` or `a` equals `b`.
`Prod.mk_lt_mk_iff_left` theorem Prod.mk_lt_mk_iff_left : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {a₁ a₂ : α} {b : β}, (a₁, b) < (a₂, b) ↔ a₁ < a₂ This theorem states that for any two elements `a1` and `a2` of a type `α`, and an element `b` of type `β`, under the condition that `α` and `β` are preordered, the ordered pair `(a1, b)` is less than the ordered pair `(a2, b)` if and only if `a1` is less than `a2`. In other words, it asserts that the comparison of two pairs in a product order is determined by the comparison of their first components when the second components are the same. More concisely: For any preordered types `α` and `β`, and all `a1, a2 : α` and `b : β`, `(a1, b) < (a2, b)` if and only if `a1 < a2` in `α`.
`rel_imp_eq_of_rel_imp_le` theorem rel_imp_eq_of_rel_imp_le : ∀ {α : Type u} {β : Type v} [inst : PartialOrder β] (r : α → α → Prop) [inst_1 : IsSymm α r] {f : α → β}, (∀ (a b : α), r a b → f a ≤ f b) → ∀ {a b : α}, r a b → f a = f b This theorem states that for any two types `α` and `β`, where `β` is a partial order, and a symmetric relation `r` on `α`, if for any two elements of `α`, the relation 'r' implies that the function `f` applied to the first element is less than or equal to `f` applied to the second element, then it must be the case that `f` applied to the first element is equal to `f` applied to the second element. In other words, if a symmetric relation implies a less-equal relation under a function, it also implies an equality under the same function. More concisely: If `β` is a partial order and `r` is a symmetric relation on `α` such that `r(x, y)` implies `f(x) ≤ f(y)` for all `x, y ∈ α`, then `f(x) = f(y)` for all `x, y ∈ α` with `r(x, y)`.
`Prod.mk_lt_mk_iff_right` theorem Prod.mk_lt_mk_iff_right : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b₁ b₂ : β}, (a, b₁) < (a, b₂) ↔ b₁ < b₂ This theorem states that for any given types `α` and `β`, where `α` and `β` are preordered, and for any elements `a` of type `α` and `b₁, b₂` of type `β`, the pair `(a, b₁)` is less than the pair `(a, b₂)` if and only if `b₁` is less than `b₂`. In other words, when the first elements of the pairs are equal (`a`), the ordering of the pairs is determined solely by the ordering of the second elements (`b₁` and `b₂`). More concisely: For any preordered types `α` and `β`, and elements `a` of type `α` and `b₁, b₂` of type `β`, `(a, b₁) < (a, b₂)` if and only if `b₁ < b₂`.
`LE.le.lt_or_eq_dec` theorem LE.le.lt_or_eq_dec : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : DecidableRel fun x x_1 => x ≤ x_1] {a b : α}, a ≤ b → a < b ∨ a = b This theorem, which is an alias of `Decidable.lt_or_eq_of_le`, is a statement about any type `α` with a partial order and a decidable relation for the "less than or equal to" operation. Given any two elements `a` and `b` of type `α`, if `a` is less than or equal to `b`, then either `a` is strictly less than `b` or `a` equals `b`. More concisely: If `α` is a type with a partial order and decidable "less than or equal to" relation, then for all `a` and `b` in `α`, if `a <= b`, then `a < b` or `a = b`.
`Mathlib.Order.Basic._auxLemma.26` theorem Mathlib.Order.Basic._auxLemma.26 : ∀ {α : Type u} [inst : LT α] {p : α → Prop} {x y : α} {hx : p x} {hy : p y}, (⟨x, hx⟩ < ⟨y, hy⟩) = (x < y) := by sorry This theorem, `Mathlib.Order.Basic._auxLemma.26`, states that for any type `α` with a less-than (`<`) operation, given a predicate `p` on `α` and two elements `x` and `y` of `α` for which the predicate `p` holds (i.e., `p x` and `p y` are both true), the inequality `{ val := x, property := hx } < { val := y, property := hy }` is equivalent to `x < y`. Here, `{ val := x, property := hx }` and `{ val := y, property := hy }` represent subtypes of `α` for which the predicate `p` holds. More concisely: For any type `α` with a total order `<` and for all `x` and `y` in `α` such that `p(x)` and `p(y)` hold, `x < y` if and only if `{x : α \| p(x)} < {y : α \| p(y)}`.
`StrongLT.lt` theorem StrongLT.lt : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → Preorder (π i)] {a b : (i : ι) → π i} [inst_1 : Nonempty ι], StrongLT a b → a < b This theorem, referred to as an alias of `lt_of_strongLT`, states that for any type `ι`, and a set of types `π` indexed by `ι`, if we have a preorder (a binary relation indicating that, for every pair of elements in the set, one of the elements precedes the other), then for any two functions `a` and `b` of type `ι` to `π`, if the function `a` is strongly less than the function `b` (meaning `a i < b i` for all `i`), then `a` is less than `b`. Note that this theorem also requires that type `ι` be nonempty. More concisely: If `ι` is nonempty and `≤` is a preorder on `π` indexed by `ι`, then `a ≤ b` implies `∀ i, a i < b i` for functions `a` and `b` from `ι` to `π`, with `a` strongly less than `b`.
`Ne.not_le_or_not_le` theorem Ne.not_le_or_not_le : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≠ b → ¬a ≤ b ∨ ¬b ≤ a This theorem states that for any type `α` that has a partial order defined on it, and for any two elements `a` and `b` of type `α`, if `a` is not equal to `b`, then either `a` is not less than or equal to `b` or `b` is not less than or equal to `a`. In other words, when two elements from a partially ordered set are distinct, at least one of them is strictly greater than the other. More concisely: For any partially ordered type `α` and elements `a` and `b` of `α`, if `a ≠ b` then neither `a ≤ b` nor `b ≤ a`.
`DenselyOrdered.dense` theorem DenselyOrdered.dense : ∀ {α : Type u} [inst : LT α] [self : DenselyOrdered α] (a₁ a₂ : α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂ This theorem states that in a densely ordered set, for any two distinct elements `a₁` and `a₂` such that `a₁` is less than `a₂`, there exists an element `a` such that `a` is greater than `a₁` and less than `a₂`. In other words, this theorem defines the property of an order being "dense" -- if we pick any two different elements in the set, there's always another element in the set that lies between them. More concisely: In a densely ordered set, between any two distinct elements lies another element.
`Subtype.mk_lt_mk` theorem Subtype.mk_lt_mk : ∀ {α : Type u} [inst : LT α] {p : α → Prop} {x y : α} {hx : p x} {hy : p y}, ⟨x, hx⟩ < ⟨y, hy⟩ ↔ x < y The theorem `Subtype.mk_lt_mk` states that for any type `α` with a less-than (`<`) operation, and for any property `p` on `α`, given two elements `x` and `y` of `α` such that `p(x)` and `p(y)` are true, the proposition that the subtype element constructed from `x` and `hx` is less than the subtype element constructed from `y` and `hy` is equivalent to the proposition that `x` is less than `y`. This theorem essentially states that the less-than relation on the original type `α` is preserved when we move to the corresponding subtype where all elements satisfy the property `p`. More concisely: Given a type `α` with a total order `<`, and a property `p` on `α`, if `x < y` and `p(x)` and `p(y)` hold, then `Subtype.mk x hx < Subtype.mk y hy` in the subtype `p ⁢ ℝ`.
`LT.lt.gt` theorem LT.lt.gt : ∀ {α : Type u} [inst : LT α] {x y : α}, x < y → y > x This theorem, referred to as `LT.lt.gt`, asserts that for all instances of a type `α` that has a less-than (`LT`) operator, if `x` and `y` are elements of this type, and if `x` is less than `y`, then `y` is greater than `x`. Essentially, this theorem states that the "less than" and "greater than" relationships are inverse of each other in the context of an ordered type. More concisely: For all types `α` with a less-than (`LT`) operator and all `x` and `y` of type `α`, if `x` is less than `y` (`x < y`), then `y` is greater than `x` (`y > x`).
`Eq.not_gt` theorem Eq.not_gt : ∀ {α : Type u} [inst : Preorder α] {x y : α}, x = y → ¬y < x This theorem, named `Eq.not_gt`, states that for any type `α` that has a preorder relationship, and for any two elements `x` and `y` of this type, if `x` equals `y`, then it is not true that `y` is less than `x`. In simple terms, if `x` and `y` are equal, `y` cannot be less than `x`, which aligns with the basic understanding of equality and ordering. More concisely: For any type with a preorder relation, if x equals y, then y is not less than x.
`le_update_iff` theorem le_update_iff : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)] {x y : (i : ι) → π i} {i : ι} {a : π i}, x ≤ Function.update y i a ↔ x i ≤ a ∧ ∀ (j : ι), j ≠ i → x j ≤ y j The theorem `le_update_iff` states that for all types `ι` and `π` (where `π` is a function of `ι`), where `ι` has decidable equality and every element of `ι` forms a preorder with `π`, for all functions `x` and `y` mapping elements of `ι` to `π`, for all elements `i` of `ι` and `a` of `π`, `x` is less than or equal to the function `y` updated at `i` with `a` if and only if the value of `x` at `i` is less than or equal to `a` and for all `j` not equal to `i`, the value of `x` at `j` is less than or equal to the value of `y` at `j`. In simpler terms, it states that a function `x` is less than or equal to another function `y` updated with a certain value at a specific point, if and only if `x`'s value at this specific point is less than or equal to the new value, and `x`'s values at all other points are less than or equal to `y`'s corresponding values. More concisely: For functions `x:` `ι` `→` `π` and `y:` `ι` `→` `π` over a preordered type `ι` with decidable equality, `x ≤ y.update i a` if and only if `x i ≤ a` and for all `j ≠ i`, `x j ≤ y j`.
`Eq.trans_le` theorem Eq.trans_le : ∀ {α : Type u} {a b c : α} [inst : LE α], a = b → b ≤ c → a ≤ c This theorem, `Eq.trans_le`, states that for any type `α` that has a less than or equal to (`≤`) operation and for any elements `a`, `b`, and `c` of this type, if `a` is equal to `b` and `b` is less than or equal to `c`, then `a` is less than or equal to `c`. In other words, it asserts the transitivity of the `≤` relation over equality, allowing to replace `b` with `a` in the inequality `b ≤ c` when `a` and `b` are equal. More concisely: If `a` equals `b` and `b` is less than or equal to `c`, then `a` is less than or equal to `c` (transitivity of the `≤` relation over equality).
`lt_of_not_le` theorem lt_of_not_le : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, ¬b ≤ a → a < b This theorem stipulates that for any type `α` which exhibits the properties of a linear order, if it is not true that `b` is less than or equal to `a`, then `a` is strictly less than `b`. In other words, for all `a` and `b` of type `α`, if `b` is not less than or equal to `a`, then `a` must be less than `b`. This theorem is an embodiment of the trichotomy property of ordered fields, which states that for any two elements in the field, either one is less than the other, they are equal, or the second is less than the first. More concisely: For any linear order type `α`, if `a` is not less than or equal to `b`, then `b` is strictly greater than `a`.
`le_implies_le_of_le_of_le` theorem le_implies_le_of_le_of_le : ∀ {α : Type u} {a b c d : α} [inst : Preorder α], c ≤ a → b ≤ d → a ≤ b → c ≤ d This theorem states that in a preorder (a set equipped with a reflexive and transitive binary relation), given any four elements `a`, `b`, `c`, and `d`, if `c` is lesser than or equal to `a`, and `b` is lesser than or equal to `d`, and `a` is lesser than or equal to `b`, then it must be the case that `c` is lesser than or equal to `d`. In other words, the "less than or equal to" relation is monotonic with respect to implication, meaning that the ordering is preserved when moving from `c` to `a` and from `b` to `d`, provided `a` is not greater than `b`. More concisely: In a preorder, if `a` is less than or equal to `b` and `b` is less than or equal to `d`, then `a` is less than or equal to `d`.
`Subtype.coe_le_coe` theorem Subtype.coe_le_coe : ∀ {α : Type u} [inst : LE α] {p : α → Prop} {x y : Subtype p}, ↑x ≤ ↑y ↔ x ≤ y The theorem `Subtype.coe_le_coe` states that for any type `α` that has a less than or equal to (`LE`) operation defined, and for any predicate `p` on `α`, for any two elements `x` and `y` of the subtype determined by `p`, the relation `x ≤ y` in the subtype is equivalent to the relation `↑x ≤ ↑y` in the original type `α`. Here, `↑x` and `↑y` denote the elements in `α` corresponding to `x` and `y`, respectively. More concisely: For any type `α` with a `LE` operation and subtype `s : Set α` defined by a predicate `p`, for all `x, y ∈ s`, `x ≤ y` if and only if `↑x ≤ ↑y` in `α`.
`update_le_iff` theorem update_le_iff : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)] {x y : (i : ι) → π i} {i : ι} {a : π i}, Function.update x i a ≤ y ↔ a ≤ y i ∧ ∀ (j : ι), j ≠ i → x j ≤ y j The theorem `update_le_iff` states that, for all index types `ι`, value types `π` (which is a function of `ι`), a decidable equality instance on `ι`, a preorder instance on each `π i`, and functions `x` and `y` from `ι` to `π i`, along with a specific index `i` and a value `a` of type `π i`, the updated function `x` with `a` at position `i` is less than or equal to `y` if and only if `a` is less than or equal to the value of `y` at index `i` and for all other indices `j` not equal to `i`, the value of `x` at `j` is less than or equal to the value of `y` at `j`. In simpler terms, updating a function at a specific index doesn't change the order relationship of the function at other indices. More concisely: For functions from an index type to a preordered type, updating one index with a value less than or equal to the existing value at that index preserves the preorder relationship with the function at all other indices.
`Mathlib.Order.Basic._auxLemma.3` theorem Mathlib.Order.Basic._auxLemma.3 : ∀ {α : Type u} [inst : Preorder α] {a b : α} [inst_1 : Subsingleton α], (a ≤ b) = True This theorem states that for any type `α` with a preorder and subsingleton structures, and any two elements `a` and `b` of type `α`, the statement "a is less than or equal to b" is always true. In other words, in a type with a preorder where there is at most one element, any two elements are always considered to be in a "less than or equal to" relationship. More concisely: In a preordered type with a subsingleton structure, any two elements are equivalent with respect to the preorder relation.
`eq_of_forall_ge_iff` theorem eq_of_forall_ge_iff : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, (∀ (c : α), a ≤ c ↔ b ≤ c) → a = b := by sorry This theorem states that for any type `α` that has a partial order, given any two elements `a` and `b` of `α`, if for every element `c` of `α`, `a` is less than or equal to `c` if and only if `b` is less than or equal to `c`, then `a` must equal `b`. In other words, if `a` and `b` have identical relationships of being less than or equal to every other element in the set, then `a` and `b` must be equal. More concisely: If `α` is a type with a partial order such that `a ≤ c` if and only if `b ≤ c` for all `c` in `α`, then `a = b`.
`min_rec'` theorem min_rec' : ∀ {α : Type u} [inst : LinearOrder α] {x y : α} (p : α → Prop), p x → p y → p (min x y) This theorem states that for any type `α` that has a linear order, given two elements `x` and `y` of type `α` and a property `p` applicable to elements of `α`, if `p` holds for `x` and `y`, then `p` also holds for the minimum of `x` and `y`. This is essentially a form of mathematical induction applied to the concept of a minimum in a linearly ordered set. More concisely: If `α` is a linearly ordered type, `x`, `y` are elements of `α`, and `p` is a property such that `p x` and `p y` hold, then `p (min x y)` also holds.
`lt_iff_lt_of_le_iff_le` theorem lt_iff_lt_of_le_iff_le : ∀ {α : Type u} {β : Type u_3} [inst : LinearOrder α] [inst_1 : LinearOrder β] {a b : α} {c d : β}, (a ≤ b ↔ c ≤ d) → (b < a ↔ d < c) This theorem states that for any two types α and β, both of which are linearly ordered, and for any respective pairs of elements (a, b) from α and (c, d) from β, if the "less than or equal to" relation between a and b is equivalent to the "less than or equal to" relation between c and d, then the "less than" relation between b and a is equivalent to the "less than" relation between d and c. In simpler words, if a is less than or equal to b exactly when c is less than or equal to d, then b is less than a exactly when d is less than c. More concisely: If two linearly ordered types α and β, and their elements a, b from α and c, d from β satisfy a ≤ b if and only if c ≤ d, then b ≤ a if and only if d ≤ c.
`LT.lt.asymm` theorem LT.lt.asymm : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → ¬b < a This theorem, also known as the alias of `lt_asymm`, states that for any type `α` with a preorder relation, given two elements `a` and `b` of that type, if `a` is less than `b`, then it cannot be the case that `b` is less than `a`. This theorem expresses the asymmetry of the 'less than' relation in a preordered set. More concisely: If `a` is less than `b` in a preordered type `α`, then it is not the case that `b` is less than `a`.
`LE.le.trans_strongLT` theorem LE.le.trans_strongLT : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → Preorder (π i)] {a b c : (i : ι) → π i}, a ≤ b → StrongLT b c → StrongLT a c This theorem, referred to as `LE.le.trans_strongLT`, states that for any index type `ι` and any family of preorder types `π` indexed by `ι`, given three functions `a`, `b`, and `c` from `ι` to `π`, if `a` is less than or equal to `b`, and `b` is strongly less than `c` (i.e., `b(i) < c(i)` for all `i` in `ι`), then `a` is also strongly less than `c`. This theorem captures one aspect of the transitivity of order relations in the context of indexed families of preorders. More concisely: If `π` is a family of preorders indexed by `ι`, and `a ≤ b` and `b < c` hold for all `i ∈ ι` in the preorder `π(i)`, then `a ≤ c` in `π(i)` for all `i ∈ ι`.
`ltByCases_eq` theorem ltByCases_eq : ∀ {α : Type u} [inst : LinearOrder α] {P : Sort u_3} {x y : α} (h : x = y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P}, ltByCases x y h₁ h₂ h₃ = h₂ h The theorem `ltByCases_eq` states that for all types `α` that are equipped with a `LinearOrder` instance and any two elements `x` and `y` of type `α`, if `x` is equal to `y`, then the result of the function `ltByCases`, which performs a case-split on the ordering of `x` and `y`, is equal to the outcome of the function `h₂`. This function `h₂` is the case function corresponding to the condition that `x` equals `y`. In essence, `ltByCases` correctly handles the case when `x` and `y` are equal by returning the result of the function that handles the equality case. More concisely: For any type `α` with a `LinearOrder` instance and elements `x` and `y` of type `α`, if `x = y`, then `ltByCases x y` equals the result of the equality case function `h₂` in the definition of `ltByCases`.
`eq_or_lt_of_le` theorem eq_or_lt_of_le : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → a = b ∨ a < b This theorem states that for any two elements 'a' and 'b' in a type 'α' with a partial order, if 'a' is less than or equal to 'b', then 'a' is either equal to 'b' or 'a' is strictly less than 'b'. Here, 'α' is a placeholder for any type that has a partial order defined on it. The PartialOrder typeclass in Lean encapsulates the properties of being reflexive, antisymmetric and transitive, which are the necessary and sufficient conditions for a relation to be a partial order. More concisely: Every relation on type 'α' with the PartialOrder typeclass is total and antisymmetric, meaning that for all 'a' and 'b' in 'α', if 'a' is less than or equal to 'b', then 'a' is equal to 'b' or strictly less than 'b'.
`LE.le.trans_eq` theorem LE.le.trans_eq : ∀ {α : Type u} {a b c : α} [inst : LE α], a ≤ b → b = c → a ≤ c This theorem, `LE.le.trans_eq`, states that for any type `α` equipped with a "less than or equal to" relation (`≤`), if we have some elements `a`, `b`, and `c` of type `α` such that `a` is less than or equal to `b` (`a ≤ b`), and `b` is equal to `c` (`b = c`), then it follows that `a` is less than or equal to `c` (`a ≤ c`). This theorem is essentially a version of the transitivity property of the `≤` relation, taking into account equality. More concisely: If `a ≤ b` and `b = c`, then `a ≤ c`. (The "less than or equal to" relation `≤` is transitive over equality.)
`Ne.le_iff_lt` theorem Ne.le_iff_lt : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≠ b → (a ≤ b ↔ a < b) This theorem states that for any given type `α` that has a partial order, and for any two elements `a` and `b` of type `α`, if `a` is not equal to `b`, then `a` is less than or equal to `b` if and only if `a` is less than `b`. In the context of mathematics, it asserts that for two unequal elements in a partially ordered set, the property of one element being less than or equal to the other is equivalent to the property of the first element being strictly less than the second. More concisely: For any partially ordered type `α` and elements `a` and `b` of type `α` with `a ≠ b`, we have `a ≤ b` if and only if `a < b`.
`associative_of_commutative_of_le` theorem associative_of_commutative_of_le : ∀ {α : Type u} [inst : PartialOrder α] {f : α → α → α}, Commutative f → (∀ (a b c : α), f (f a b) c ≤ f a (f b c)) → Associative f This theorem states that for any type `α` equipped with a partial ordering, if we have a binary operation `f` that is commutative, and for all `a`, `b`, and `c` of type `α`, the result of first applying `f` to `a` and `b` and then applying `f` to that result and `c` is less than or equal to the result of applying `f` to `a` and the result of applying `f` to `b` and `c`, then `f` is associative. In mathematical terms, if `f` is a commutative operation such that `(f(a, b), c) ≤ f(a, (b, c))` for all `a`, `b`, `c`, then `f` is associative, meaning that `f(f(a, b), c) = f(a, f(b, c))`. More concisely: If a commutative binary operation `f` on a partially ordered type satisfies the condition that `f(a, b) <= f(a, c) & f(c, b)` for all `a, b, c`, then `f` is associative, that is, `f(f(a, b), c) = f(a, f(b, c))`.
`lt_iff_le_and_ne` theorem lt_iff_le_and_ne : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a < b ↔ a ≤ b ∧ a ≠ b This theorem states that for any type `α` that has a defined partial order, and for any two elements `a` and `b` of that type, `a` is less than `b` if and only if both `a` is less than or equal to `b` and `a` is not equal to `b`. In other words, in the context of a partial order, strict less than (`a < b`) is equivalent to the conjunction of less than or equal (`a ≤ b`) and inequality (`a ≠ b`). More concisely: For any type `α` with a partial order, `a < b` if and only if `a ≤ b` and `a ≠ b`.
`Eq.not_lt` theorem Eq.not_lt : ∀ {α : Type u} [inst : Preorder α] {x y : α}, x = y → ¬x < y This theorem states that for any type `α` that has a preorder (a mathematical model that can describe an ordering among its elements), and for any two elements `x` and `y` from that type, if `x` is equal to `y`, then `x` is not less than `y`. In other words, an element cannot be less than itself in a preorder, reflecting the antisymmetry property of preorders in mathematical terms. More concisely: In a preorder, for all types `α` and elements `x` and `y` of type `α`, if `x = y`, then `x ≤ y` implies `y ≤ x`.

LeanAide GPT-4 documentation

Module: Mathlib.Order.Basic

Eq.trans_gt

theorem Eq.trans_gt : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, b = c → a < b → a < c

Ne.lt_or_lt

theorem Ne.lt_or_lt : ∀ {α : Type u} [inst : LinearOrder α] {x y : α}, x ≠ y → x < y ∨ y < x

StrongLT.le

theorem StrongLT.le : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → Preorder (π i)] {a b : (i : ι) → π i}, StrongLT a b → a ≤ b

le_of_forall_ge_of_dense

theorem le_of_forall_ge_of_dense : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] {a₁ a₂ : α}, (∀ a₃ < a₁, a₃ ≤ a₂) → a₁ ≤ a₂ := by sorry

le_of_forall_lt

theorem le_of_forall_lt : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, (∀ c < a, c < b) → a ≤ b

lt_of_le_of_ne'

theorem lt_of_le_of_ne' : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≠ a → a < b

LE.le.eq_or_lt_dec

theorem LE.le.eq_or_lt_dec : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : DecidableRel fun x x_1 => x ≤ x_1] {a b : α}, a ≤ b → a = b ∨ a < b

LT.lt.trans_eq

theorem LT.lt.trans_eq : ∀ {α : Type u} {a b c : α} [inst : LT α], a < b → b = c → a < c

LT.lt.not_lt

theorem LT.lt.not_lt : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → ¬b < a

le_iff_eq_or_lt

theorem le_iff_eq_or_lt : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b ↔ a = b ∨ a < b

le_trans'

theorem le_trans' : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, b ≤ c → a ≤ b → a ≤ c

le_iff_le_iff_lt_iff_lt

theorem le_iff_le_iff_lt_iff_lt : ∀ {α : Type u} {β : Type u_3} [inst : LinearOrder α] [inst_1 : LinearOrder β] {a b : α} {c d : β}, (a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c)

LT.lt.ne'

theorem LT.lt.ne' : ∀ {α : Type u} [inst : Preorder α] {x y : α}, x < y → y ≠ x

lt_imp_lt_of_le_imp_le

theorem lt_imp_lt_of_le_imp_le : ∀ {α : Type u} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} {c d : β}, (a ≤ b → c ≤ d) → d < c → b < a

LT.lt.lt_or_lt

theorem LT.lt.lt_or_lt : ∀ {α : Type u} [inst : LinearOrder α] {x y : α}, x < y → ∀ (z : α), x < z ∨ z < y

eq_of_le_of_not_lt

theorem eq_of_le_of_not_lt : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → ¬a < b → a = b

LT.lt.le

theorem LT.lt.le : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → a ≤ b

Function.const_lt_const

theorem Function.const_lt_const : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Nonempty β] {a b : α}, Function.const β a < Function.const β b ↔ a < b

Mathlib.Order.Basic._auxLemma.1

theorem Mathlib.Order.Basic._auxLemma.1 : ∀ {α : Type u} [inst : Preorder α] (a : α), (a ≤ a) = True

le_of_strongLT

theorem le_of_strongLT : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → Preorder (π i)] {a b : (i : ι) → π i}, StrongLT a b → a ≤ b

Eq.trans_lt

theorem Eq.trans_lt : ∀ {α : Type u} {a b c : α} [inst : LT α], a = b → b < c → a < c

ltByCases_gt

theorem ltByCases_gt : ∀ {α : Type u} [inst : LinearOrder α] {P : Sort u_3} {x y : α} (h : y < x) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P}, ltByCases x y h₁ h₂ h₃ = h₃ h

LE.le.lt_iff_ne

theorem LE.le.lt_iff_ne : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → (a < b ↔ a ≠ b)

Preorder.toLE_injective

theorem Preorder.toLE_injective : ∀ {α : Type u_3}, Function.Injective (@Preorder.toLE α)

LE.ext

theorem LE.ext : ∀ {α : Type u} (x y : LE α), LE.le = LE.le → x = y

not_le_of_lt

theorem not_le_of_lt : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a

Eq.ge

theorem Eq.ge : ∀ {α : Type u} [inst : Preorder α] {x y : α}, x = y → y ≤ x

lt_iff_lt_of_le_iff_le'

theorem lt_iff_lt_of_le_iff_le' : ∀ {α : Type u} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} {c d : β}, (a ≤ b ↔ c ≤ d) → (b ≤ a ↔ d ≤ c) → (b < a ↔ d < c)

Eq.le

theorem Eq.le : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a = b → a ≤ b

LE.le.trans

theorem LE.le.trans : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c

Subtype.coe_lt_coe

theorem Subtype.coe_lt_coe : ∀ {α : Type u} [inst : LT α] {p : α → Prop} {x y : Subtype p}, ↑x < ↑y ↔ x < y

LT.lt.trans_le

theorem LT.lt.trans_le : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, a < b → b ≤ c → a < c

LE.le.le_iff_eq

theorem LE.le.le_iff_eq : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a ≤ b → (b ≤ a ↔ b = a)

exists_forall_ge_and

theorem exists_forall_ge_and : ∀ {α : Type u} [inst : LinearOrder α] {p q : α → Prop}, (∃ i, ∀ j ≥ i, p j) → (∃ i, ∀ j ≥ i, q j) → ∃ i, ∀ j ≥ i, p j ∧ q j

ltByCases_lt

theorem ltByCases_lt : ∀ {α : Type u} [inst : LinearOrder α] {P : Sort u_3} {x y : α} (h : x < y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P}, ltByCases x y h₁ h₂ h₃ = h₁ h

LT.lt.trans_eq'

theorem LT.lt.trans_eq' : ∀ {α : Type u} [inst : Preorder α] {a b c : α}, b < c → a = b → a < c

ge_of_eq

theorem ge_of_eq : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a = b → a ≥ b

max_def'

theorem max_def' : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), max a b = if b ≤ a then a else b

eq_iff_le_not_lt

theorem eq_iff_le_not_lt : ∀ {α : Type u} [inst : PartialOrder α] {a b : α}, a = b ↔ a ≤ b ∧ ¬a < b

`Eq.trans_gt`

`Ne.lt_or_lt`

`StrongLT.le`

`le_of_forall_ge_of_dense`

`le_of_forall_lt`

`lt_of_le_of_ne'`

`LE.le.eq_or_lt_dec`

`LT.lt.trans_eq`

`LT.lt.not_lt`

`le_iff_eq_or_lt`

`le_trans'`

`le_iff_le_iff_lt_iff_lt`

`LT.lt.ne'`

`lt_imp_lt_of_le_imp_le`

`LT.lt.lt_or_lt`

`eq_of_le_of_not_lt`

`LT.lt.le`

`Function.const_lt_const`

`Mathlib.Order.Basic._auxLemma.1`

`le_of_strongLT`

`Eq.trans_lt`

`ltByCases_gt`

`LE.le.lt_iff_ne`

`Preorder.toLE_injective`

`LE.ext`

`not_le_of_lt`

`Eq.ge`

`lt_iff_lt_of_le_iff_le'`

`Eq.le`

`LE.le.trans`

`Subtype.coe_lt_coe`

`LT.lt.trans_le`

`LE.le.le_iff_eq`

`exists_forall_ge_and`

`ltByCases_lt`

`LT.lt.trans_eq'`

`ge_of_eq`

`max_def'`

`eq_iff_le_not_lt`

`LE.le.trans'`

`max_rec'`

`eq_of_le_of_forall_le_of_dense`

`LE.le.trans_lt'`

`LT.lt.not_le`

`LE.le.eq_of_not_gt`

`exists_between`

`StrongLT.trans_le`

`LT.lt.trans'`

`ge_antisymm`

`lt_self_iff_false`

`LE.le.eq_or_gt`

`PartialOrder.ext`

`not_lt_of_le`

`LE.le.trans_lt`

`GT.gt.lt`

`eq_or_eq_or_eq_of_forall_not_lt_lt`

`LT.lt.ne`

`LE.le.trans_eq'`

`Pi.lt_def`

`Ne.lt_of_le`

`eq_of_forall_le_iff`

`LT.lt.trans`

`LE.le.eq_of_not_lt`

`LE.le.antisymm`

`Mathlib.Order.Basic._auxLemma.2`

`LE.le.eq_or_lt`

`Function.const_le_const`

`lt_or_lt_iff_ne`

`LE.le.gt_iff_ne`

`LT.lt.false`

`Mathlib.Order.Basic._auxLemma.25`

`le_of_forall_lt'`

`LE.le.lt_of_ne'`

`Mathlib.Order.Basic._auxLemma.10`