Mathlib.Data.Sum.Order._auxLemma.3
theorem Mathlib.Data.Sum.Order._auxLemma.3 :
∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a b : α}, (Sum.inl a < Sum.inl b) = (a < b) := by
sorry
This theorem from the Mathlib library in Lean 4 states that for any types `α` and `β`, provided `α` and `β` have a less than (`<`) operation, and for any two elements `a` and `b` of type `α`, the inequality `Sum.inl a < Sum.inl b` (where `Sum.inl` constructs a sum type from the left component) is equivalent to `a < b`. Essentially, it says that comparing two elements in the sum type where both elements come from the left type is the same as just comparing the elements in the original type.
More concisely: For any types `α` with a total order and any `a, b : α`, `Sum.inl a < Sum.inl b` if and only if `a < b`.
|
Mathlib.Data.Sum.Order._auxLemma.14
theorem Mathlib.Data.Sum.Order._auxLemma.14 :
∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a b : α ⊕ β},
(toLex a ≤ toLex b) = Sum.Lex (fun x x_1 => x ≤ x_1) (fun x x_1 => x ≤ x_1) a b
The theorem `Mathlib.Data.Sum.Order._auxLemma.14` states that for any two elements `a` and `b` of the sum type `α ⊕ β`, where `α` and `β` are types with a less than or equal to (≤) relation, the statement that `a` is less than or equal to `b` under the `toLex` function (which essentially treats `a` and `b` as elements of the lexicographic order type `Lex α`) is equivalent to the statement that `a` is less than or equal to `b` under the sum lexicographic order `Sum.Lex`, where the ordering on both components is the less than or equal to relation of the respective types.
More concisely: For any `a : α ⊕ β` and `b : α ⊕ β` in a sum type with types `α` and `β` ordered by a relation ≤, `a ≤ b` under the `toLex` function is equivalent to `a ≤ b` under the sum lexicographic order `Sum.Lex` with respect to the ordering ≤ on both components.
|
Mathlib.Data.Sum.Order._auxLemma.6
theorem Mathlib.Data.Sum.Order._auxLemma.6 :
∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a : α} {b : β}, (Sum.inl b < Sum.inr a) = False := by
sorry
This theorem from Mathlib, named `Mathlib.Data.Sum.Order._auxLemma.6`, states that for any two types `α` and `β` that have a less-than (`<`) relation defined on them, any value `b` of type `β` wrapped in a `Sum.inl` is not less than any value `a` of type `α` wrapped in a `Sum.inr`. In other words, no `Sum.inl b` can be less than `Sum.inr a` under any circumstances. This theorem is part of the formalization of order relations on sum types in Lean.
More concisely: For any types `α` and `β` with a defined less-than relation, `Sum.inl b < Sum.inr a` does not hold for any `a : α` and `b : β`.
|
Mathlib.Data.Sum.Order._auxLemma.1
theorem Mathlib.Data.Sum.Order._auxLemma.1 :
∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a b : α}, (Sum.inl a ≤ Sum.inl b) = (a ≤ b) := by
sorry
This theorem, `Mathlib.Data.Sum.Order._auxLemma.1`, states that for any two types `α` and `β`, both of which have a less than or equal to (`≤`) operation, and for any two elements `a` and `b` of type `α`, the condition that `a` is less than or equal to `b` under the `Sum.inl` operation is equivalent to the condition that `a` is less than or equal to `b`. In other words, the ordering of the elements `a` and `b` remains the same whether we're considering them as elements of type `α` or as elements of the co-product type `α + β`.
More concisely: For any types `α` and `β` with a `≤` operation, and for all `a : α` and `b : α`, `a ≤ a + b` if and only if `a ≤ b`.
|
Sum.Lex.inl_le_inl_iff
theorem Sum.Lex.inl_le_inl_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a b : α},
toLex (Sum.inl a) ≤ toLex (Sum.inl b) ↔ a ≤ b
This theorem states that for any two objects `a` and `b` of a certain type `α`, the inequality of `toLex (Sum.inl a)` and `toLex (Sum.inl b)` is equivalent to the inequality of `a` and `b` themselves. Here, `toLex` is a function that just renames its input as the Lex type, `Sum.inl` is a function that injects its input into the left component of a sum type, and `≤` denotes a general notion of "less than or equal to". The theorem holds in the context where `α` and `β` are any types, and `α` has a specified "less than or equal to" relation.
More concisely: For any type `α` with a "less than or equal to" relation, and for all objects `a` and `b` of type `α`, `toLex (Sum.inl a) ≤ toLex (Sum.inl b)` if and only if `a ≤ b`.
|
Sum.Lex.inr_le_inr_iff
theorem Sum.Lex.inr_le_inr_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a b : β},
toLex (Sum.inr a) ≤ toLex (Sum.inr b) ↔ a ≤ b
This theorem, `Sum.Lex.inr_le_inr_iff`, asserts that for any two types `α` and `β` with a less than or equal to order (`LE`), and for any two elements `a` and `b` of type `β`, the `toLex` function applied to `Sum.inr a` is less than or equal to the `toLex` function applied to `Sum.inr b` if and only if `a` is less than or equal to `b`. Here, `Sum.inr` is a function that injects `β` into the sum type `α ⊕ β`. The `toLex` function is an identity function that maps elements of a type to their lexicographical ordering.
More concisely: For all types `α ≤ β` and elements `a ∈ β`, `toLex (Sum.inr a) ≤ toLex (Sum.inr b)` if and only if `a ≤ b` in `β`.
|
Mathlib.Data.Sum.Order._auxLemma.8
theorem Mathlib.Data.Sum.Order._auxLemma.8 :
∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a : α} {b : β}, (Sum.inr b < Sum.inl a) = False := by
sorry
This theorem states that for any types `α` and `β` that have defined "less than" (`<`) operations, and for any instances `a` of type `α` and `b` of type `β`, it is always false that `b` (wrapped in the `Sum.inr` constructor) is less than `a` (wrapped in the `Sum.inl` constructor). In other words, no right element of a sum type is less than any left element of the sum type.
More concisely: For all types `α` and `β` with defined "<" operations, and for all `a : α` and `b : β`, `Sum.inr b < Sum.inl a` always holds false.
|
Mathlib.Data.Sum.Order._auxLemma.5
theorem Mathlib.Data.Sum.Order._auxLemma.5 :
∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a : α} {b : β}, (Sum.inl b ≤ Sum.inr a) = False := by
sorry
The theorem `Mathlib.Data.Sum.Order._auxLemma.5` states that for any types `α` and `β` that have a less than or equal to (`≤`) order defined, and any elements `a` from `α` and `b` from `β`, it is not possible for `b` of the left sum (`Sum.inl b`) to be less than or equal to `a` of the right sum (`Sum.inr a`). In other words, an element from the left part of a sum type cannot be less than or equal to an element from the right part of the sum type. This theorem is part of the order properties of sum types in Lean's mathematical library.
More concisely: For any types `α` and `β` with defined order, and elements `a : α` and `b : β`, `Sum.inl b ≤ Sum.inr a` is false.
|
Sum.inl_lt_inl_iff
theorem Sum.inl_lt_inl_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a b : α}, Sum.inl a < Sum.inl b ↔ a < b
This theorem states that for any two types `α` and `β` which both have a less-than relation defined (`LT α` and `LT β`), given two elements `a` and `b` of type `α`, the "less than" relationship between `Sum.inl a` and `Sum.inl b` (where `Sum.inl` is a function that injects `α` into the sum type `α + β`) is equivalent to the "less than" relationship between `a` and `b`. In other words, `Sum.inl a` is less than `Sum.inl b` if and only if `a` is less than `b`.
More concisely: For types `α` and `β` equipped with a less-than relation, and elements `a : α` and `b : β`, `Sum.inl a < Sum.inl b` if and only if `a < b`.
|
Sum.inr_lt_inr_iff
theorem Sum.inr_lt_inr_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a b : β}, Sum.inr a < Sum.inr b ↔ a < b
This theorem states that for any two types `α` and `β`, where the `<` (less than) relation is defined on both `α` and `β`, and for any two instances `a` and `b` of type `β`, the sum type instance `Sum.inr a` is less than `Sum.inr b` if and only if `a` is less than `b`. In other words, the ordering of the instances in the sum type `Sum.inr` is preserved from the original type `β`.
More concisely: For any types `α` with a defined `<` relation and instances `a` and `b` of type `β`, where `<` is defined, `Sum.inr a < Sum.inr b` if and only if `a < b`.
|
Sum.Lex.inr_lt_inr_iff
theorem Sum.Lex.inr_lt_inr_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a b : β},
toLex (Sum.inr a) < toLex (Sum.inr b) ↔ a < b
This theorem states that for any two types `α` and `β` with a less-than (`<`) relation, and any two elements `a` and `b` of type `β`, the statement "the lexical order of `a` is less than the lexical order of `b`" is equivalent to the statement "a is less than b". Here, the `toLex` function is used to convert `a` and `b` to their lexical orders, and `Sum.inr` is used to inject elements of type `β` into a sum type.
More concisely: For any types `α` with a `<` relation and elements `a` and `b` of type `β`, `a < b` if and only if `toLex (Sum.inr a)` is less than `toLex (Sum.inr b)` in the lexical order of `α`.
|
Sum.Lex.inl_le_inr
theorem Sum.Lex.inl_le_inr :
∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (a : α) (b : β),
toLex (Sum.inl a) ≤ toLex (Sum.inr b)
The theorem `Sum.Lex.inl_le_inr` states that for any two types `α` and `β` that have a less than or equal to (`LE`) relation defined on them, for any element `a` of type `α` and any element `b` of type `β`, the Lex (lexicographic order) of the sum type element formed by injecting `a` into the left (`Sum.inl a`) is always less than or equal to the Lex of the sum type element formed by injecting `b` into the right (`Sum.inr b`). This essentially captures the idea that in a lexicographic ordering, elements from the left component of a sum type are considered 'smaller' than elements from the right component.
More concisely: For any types `α` and `β` with a defined LE relation, and for all `a : α` and `b : β`, `Sum.inl a ≤ Sum.inr b` holds in the lexicographic order on the sum type `α + β`.
|
Sum.Lex.inl_lt_inr
theorem Sum.Lex.inl_lt_inr :
∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] (a : α) (b : β),
toLex (Sum.inl a) < toLex (Sum.inr b)
The theorem `Sum.Lex.inl_lt_inr` states that for any two types `α` and `β`, given an instance of the "less than" relation for `α` and `β`, and any elements `a` of type `α` and `b` of type `β`, the lex (lexicographic order) of the element `a` injected into the sum type with `Sum.inl` is less than the lex of the element `b` injected with `Sum.inr`. In other words, it claims that in the lexicographic ordering, all elements of the left summand are considered less than all elements of the right summand.
More concisely: For any types `α` and `β` with a defined less-than relation, and for any elements `a : α` and `b : β`, `Sum.inl a < Sum.inr b` holds in the lexicographic order on the sum type `Sum α β`.
|
Sum.Lex.inl_lt_inl_iff
theorem Sum.Lex.inl_lt_inl_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a b : α},
toLex (Sum.inl a) < toLex (Sum.inl b) ↔ a < b
This theorem, `Sum.Lex.inl_lt_inl_iff`, states that for any two types `α` and `β` equipped with a less than relation (`<`), the `toLex` function applied to the injection of an element `a` from `α` into the sum type (`Sum.inl a`) is less than the `toLex` function applied to the injection of another element `b` from `α` into the sum type (`Sum.inl b`) if and only if `a` is less than `b`. In other words, the `toLex` function preserves the order of elements when they are injected into the sum type using `Sum.inl`.
More concisely: For any types `α` equipped with a total order `<`, and for all `a` and `b` in `α`, `Sum.inl a < Sum.inl b` in the lexicographic order on `Sum α` if and only if `a < b` in `α`.
|
Mathlib.Data.Sum.Order._auxLemma.4
theorem Mathlib.Data.Sum.Order._auxLemma.4 :
∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a b : β}, (Sum.inr a < Sum.inr b) = (a < b) := by
sorry
This theorem, named `Mathlib.Data.Sum.Order._auxLemma.4`, states that for any types `α` and `β` where `α` and `β` have a less-than (`<`) relation defined, the less-than relation between 'right' elements (`Sum.inr`) of the sum type is equivalent to the less-than relation between the elements themselves. Specifically, if `a` and `b` are elements of type `β`, then `Sum.inr a` is less than `Sum.inr b` if and only if `a` is less than `b`. This theorem essentially connects the comparison operation in the context of the sum type with the comparison operation in the original type.
More concisely: For types `α` and `β` with a defined less-than relation, the less-than relation between `Sum.inr a` and `Sum.inr b` of type `Sum α β` holds if and only if `a` is less than `b` in type `β`.
|
Mathlib.Data.Sum.Order._auxLemma.7
theorem Mathlib.Data.Sum.Order._auxLemma.7 :
∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a : α} {b : β}, (Sum.inr b ≤ Sum.inl a) = False := by
sorry
This theorem is stating that for any types `α` and `β` with a less than or equal to (`≤`) relation defined on them, and for any elements `a` of type `α` and `b` of type `β`, the statement "`b` is less than or equal to `a`" is always false when `b` is considered a "right" value (`Sum.inr`) and `a` is considered a "left" value (`Sum.inl`). In other words, a right value is never less than or equal to a left value in the sum type based on `α` and `β`.
More concisely: For any types `α` and `β` with a defined `≤` relation, and for any `a : α` and `b : β`, `Sum.inr b ≤ Sum.inl a` always falsifies.
|
Sum.not_inl_lt_inr
theorem Sum.not_inl_lt_inr :
∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a : α} {b : β}, ¬Sum.inl b < Sum.inr a
This theorem states that, for any types `α` and `β` equipped with a less than (`<`) relation, and any elements `a` of type `α` and `b` of type `β`, it is not the case that `b` labelled as an element of `β` in a sum type is less than `a` labelled as an element of `α` in the same sum type. In other words, if you have two elements from different types and you put them into a sum type, you cannot say that the one from the second type is less than the one from the first type. The theorem holds for any types that have a less than relation defined.
More concisely: For any types `α` and `β` with a defined `<` relation and any `a : α` and `b : β`, `a < b` is not provable.
|
Mathlib.Data.Sum.Order._auxLemma.2
theorem Mathlib.Data.Sum.Order._auxLemma.2 :
∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a b : β}, (Sum.inr a ≤ Sum.inr b) = (a ≤ b) := by
sorry
The theorem `Mathlib.Data.Sum.Order._auxLemma.2` states that for any types `α` and `β` where `α` and `β` have a less than or equal to (`≤`) relation defined on them, and for any elements `a` and `b` of type `β`, the statement that `a` is less than or equal to `b` within the `Sum.inr` context (i.e., `Sum.inr a ≤ Sum.inr b`) is equivalent to the statement that `a` is less than or equal to `b` without the `Sum.inr` context (i.e., `a ≤ b`). In other words, wrapping `a` and `b` in `Sum.inr` doesn't change their comparison outcome.
More concisely: For any types `α` with a defined `≤` relation and elements `a` and `b` of type `β`, `Sum.inr a ≤ Sum.inr b` if and only if `a ≤ b`.
|