Sum.lex_inr_inl
theorem Sum.lex_inr_inl :
∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop} {b : β} {a : α},
¬Sum.Lex r s (Sum.inr b) (Sum.inl a)
This theorem states that for any types `α` and `β`, any binary relations `r` on `α` and `s` on `β`, and any elements `a` of `α` and `b` of `β`, it is not possible for the lexicographical order `Sum.Lex r s` of the sum type `α ⊕ β` to order `Sum.inr b` (a value from `β`) before `Sum.inl a` (a value from `α`). In other words, values from `α` (wrapped in `Sum.inl`) will always come before values from `β` (wrapped in `Sum.inr`) in this lexicographical order.
More concisely: For any binary relations r on type α and s on type β, the lexicographical order Sum.Lex r s does not order Sum.inr b before Sum.inl a for any types α, β, elements a from α, and b from β.
|
Sum.lex_inl_inl
theorem Sum.lex_inl_inl :
∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop} {a₁ a₂ : α},
Sum.Lex r s (Sum.inl a₁) (Sum.inl a₂) ↔ r a₁ a₂
This theorem, `Sum.lex_inl_inl`, is about the properties of the lexicographic order of sums in the context of two arbitrary types `α` and `β`, which are ordered by relations `r` and `s` respectively. Specifically, it states that for all elements `a₁` and `a₂` of type `α`, the lexicographic order `Sum.Lex r s` applied to the left-injections (`Sum.inl`) of `a₁` and `a₂` is equivalent to applying the relation `r` to `a₁` and `a₂` directly. In other words, ordering the left-injected sums is the same as ordering the elements themselves according to `r`.
More concisely: For types `α` ordered by relation `r` and `β` ordered by relation `s`, the lexicographic order of the left-injections of `α` applied to elements `a₁` and `a₂` is equivalent to applying `r` directly to `a₁` and `a₂`. That is, `Sum.inl a₁ <~ Sum.Lex r s Sum.inl a₂` if and only if `a₁ r a₂`.
|