Lemmas about inequalities
This file contains some lemmas about ≤/≥/</>, and cmp.
We simplify
a ≥ banda > btob ≤ aandb < a, respectively. This way we can formulate all lemmas using≤/<avoiding duplication.In some cases we introduce dot syntax aliases so that, e.g., from
(hab : a ≤ b) (hbc : b ≤ c) (hbc' : b < c)one can provehab.trans hbc : a ≤ candhab.trans_lt hbc' : a < c.
theorem
lt_imp_lt_of_le_imp_le
{α : Type u}
{β : Type u_1}
[linear_order α]
[preorder β]
{a b : α}
{c d : β} :
theorem
le_imp_le_of_lt_imp_lt
{α : Type u}
{β : Type u_1}
[preorder α]
[linear_order β]
{a b : α}
{c d : β} :
theorem
le_imp_le_iff_lt_imp_lt
{α : Type u}
{β : Type u_1}
[linear_order α]
[linear_order β]
{a b : α}
{c d : β} :
theorem
lt_iff_lt_of_le_iff_le
{α : Type u}
{β : Type u_1}
[linear_order α]
[linear_order β]
{a b : α}
{c d : β} :
theorem
le_iff_le_iff_lt_iff_lt
{α : Type u}
{β : Type u_1}
[linear_order α]
[linear_order β]
{a b : α}
{c d : β} :
theorem
decidable.lt_or_eq_of_le
{α : Type u}
[partial_order α]
[decidable_rel has_le.le]
{a b : α} :
theorem
decidable.eq_or_lt_of_le
{α : Type u}
[partial_order α]
[decidable_rel has_le.le]
{a b : α} :
theorem
decidable.le_iff_lt_or_eq
{α : Type u}
[partial_order α]
[decidable_rel has_le.le]
{a b : α} :
Perform a case-split on the ordering of x and y in a decidable linear order.
theorem
decidable.le_imp_le_of_lt_imp_lt
{α : Type u}
{β : Type u_1}
[preorder α]
[decidable_linear_order β]
{a b : α}
{c d : β} :
theorem
decidable.le_imp_le_iff_lt_imp_lt
{α : Type u}
{β : Type u_1}
[linear_order α]
[decidable_linear_order β]
{a b : α}
{c d : β} :
theorem
decidable.le_iff_le_iff_lt_iff_lt
{α : Type u}
{β : Type u_1}
[decidable_linear_order α]
[decidable_linear_order β]
{a b : α}
{c d : β} :
@[simp]
compares o a b means that a and b have the ordering relation
o between them, assuming that the relation a < b is defined
Equations
- ordering.gt.compares a b = (a > b)
- ordering.eq.compares a b = (a = b)
- ordering.lt.compares a b = (a < b)
theorem
ordering.compares.eq_lt
{α : Type u}
[preorder α]
{o : ordering}
{a b : α} :
o.compares a b → (o = ordering.lt ↔ a < b)
theorem
ordering.compares.eq_eq
{α : Type u}
[preorder α]
{o : ordering}
{a b : α} :
o.compares a b → (o = ordering.eq ↔ a = b)
theorem
ordering.compares.eq_gt
{α : Type u}
[preorder α]
{o : ordering}
{a b : α} :
o.compares a b → (o = ordering.gt ↔ b < a)
theorem
ordering.or_else_eq_lt
(o₁ o₂ : ordering) :
o₁.or_else o₂ = ordering.lt ↔ o₁ = ordering.lt ∨ o₁ = ordering.eq ∧ o₂ = ordering.lt