@[inline]
Pull back a comparator by a function f
, by applying the comparator to both arguments.
Equations
- Ordering.byKey f cmp a b = cmp (f a) (f b)
Instances For
theorem
Batteries.compareOfLessAndEq_eq_lt
{α : Type u_1}
{x y : α}
[LT α]
[Decidable (x < y)]
[DecidableEq α]
:
Batteries features not in core Std
theorem
Std.OrientedCmp.le_iff_ge
{α : Type u_1}
{cmp : α → α → Ordering}
[OrientedCmp cmp]
{x y : α}
:
theorem
Std.TransCmp.le_trans
{α : Type u_1}
{cmp : α → α → Ordering}
[TransCmp cmp]
{x y z : α}
:
cmp x y ≠ Ordering.gt → cmp y z ≠ Ordering.gt → cmp x z ≠ Ordering.gt
theorem
Std.TransCmp.lt_of_lt_of_le
{α : Type u_1}
{cmp : α → α → Ordering}
[TransCmp cmp]
{x y z : α}
:
cmp x y = Ordering.lt → cmp y z ≠ Ordering.gt → cmp x z = Ordering.lt
theorem
Std.TransCmp.lt_of_le_of_lt
{α : Type u_1}
{cmp : α → α → Ordering}
[TransCmp cmp]
{x y z : α}
:
cmp x y ≠ Ordering.gt → cmp y z = Ordering.lt → cmp x z = Ordering.lt
theorem
Std.TransCmp.ge_trans
{α : Type u_1}
{cmp : α → α → Ordering}
[TransCmp cmp]
{x y z : α}
:
cmp x y ≠ Ordering.lt → cmp y z ≠ Ordering.lt → cmp x z ≠ Ordering.lt
theorem
Std.TransCmp.gt_of_gt_of_ge
{α : Type u_1}
{cmp : α → α → Ordering}
[TransCmp cmp]
{x y z : α}
:
cmp x y = Ordering.gt → cmp y z ≠ Ordering.lt → cmp x z = Ordering.gt
theorem
Std.TransCmp.gt_of_ge_of_gt
{α : Type u_1}
{cmp : α → α → Ordering}
[TransCmp cmp]
{x y z : α}
:
cmp x y ≠ Ordering.lt → cmp y z = Ordering.gt → cmp x z = Ordering.gt
LawfulLTCmp cmp
asserts that cmp x y = .lt
and x < y
coincide.
cmp x y = .lt
holds iffx < y
is true.
Instances
theorem
Std.LawfulLTCmp.eq_gt_iff_gt
{α : Type u_1}
{cmp : α → α → Ordering}
{x y : α}
[LT α]
[LawfulLTCmp cmp]
:
LawfulLECmp cmp
asserts that (cmp x y).isLE
and x ≤ y
coincide.
cmp x y ≠ .gt
holds iffx ≤ y
is true.
Instances
theorem
Std.LawfulLECmp.ne_gt_iff_le
{α : Type u_1}
{cmp : α → α → Ordering}
{x y : α}
[LE α]
[LawfulLECmp cmp]
:
theorem
Std.LawfulLECmp.ne_lt_iff_ge
{α : Type u_1}
{cmp : α → α → Ordering}
{x y : α}
[LE α]
[LawfulLECmp cmp]
:
class
Std.LawfulBCmp
{α : Type u_1}
[LE α]
[LT α]
[BEq α]
(cmp : α → α → Ordering)
extends Std.TransCmp cmp, Std.LawfulBEqCmp cmp, Std.LawfulLTCmp cmp, Std.LawfulLECmp cmp :
LawfulBCmp cmp
asserts that the LE
, LT
, BEq
are all coherent with each other
and with cmp
, describing a strict weak order (a linear order except for antisymmetry).
Instances
class
Std.LawfulCmp
{α : Type u_1}
[LE α]
[LT α]
(cmp : α → α → Ordering)
extends Std.TransCmp cmp, Std.LawfulEqCmp cmp, Std.LawfulLTCmp cmp, Std.LawfulLECmp cmp :
LawfulBCmp cmp
asserts that the LE
, LT
, Eq
are all coherent with each other
and with cmp
, describing a linear order.
Instances
@[reducible, inline]
Class for types where the ordering function is compatible with the LT
.
Equations
Instances For
@[reducible, inline]
Class for types where the ordering function is compatible with the LE
.
Equations
Instances For
instance
Std.instOrientedCmpFlipOrdering_batteries
{α✝ : Type u_1}
{cmp : α✝ → α✝ → Ordering}
[inst : OrientedCmp cmp]
:
OrientedCmp (flip cmp)
instance
Std.instOrientedCmpByKey
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(cmp : β → β → Ordering)
[OrientedCmp cmp]
:
OrientedCmp (Ordering.byKey f cmp)
instance
Std.instTransCmpByKey
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(cmp : β → β → Ordering)
[TransCmp cmp]
:
TransCmp (Ordering.byKey f cmp)
instance
Std.instOrientedCmpCompareLex_batteries
{α✝ : Type u_1}
{cmp₁ cmp₂ : α✝ → α✝ → Ordering}
[inst₁ : OrientedCmp cmp₁]
[inst₂ : OrientedCmp cmp₂]
:
OrientedCmp (compareLex cmp₁ cmp₂)
instance
Std.instTransCmpCompareLex_batteries
{α✝ : Type u_1}
{cmp₁ cmp₂ : α✝ → α✝ → Ordering}
[inst₁ : TransCmp cmp₁]
[inst₂ : TransCmp cmp₂]
:
TransCmp (compareLex cmp₁ cmp₂)
instance
Std.instOrientedCmpCompareOnOfOrientedOrd_batteries
{β : Type u_1}
{α : Type u_2}
[Ord β]
[OrientedOrd β]
(f : α → β)
:
OrientedCmp (compareOn f)
theorem
Std.OrientedOrd.instOn
{β : Type u_1}
{α : Type u_2}
[ord : Ord β]
[OrientedOrd β]
(f : α → β)
:
theorem
Std.OrientedOrd.instOrdLex'
{α : Type u_1}
(ord₁ ord₂ : Ord α)
[OrientedOrd α]
[OrientedOrd α]
:
theorem
Std.LawfulLTCmp.eq_compareOfLessAndEq
{α : Type u_1}
{cmp : α → α → Ordering}
[LT α]
[DecidableEq α]
[LawfulEqCmp cmp]
[LawfulLTCmp cmp]
(x y : α)
[Decidable (x < y)]
:
theorem
Std.ReflCmp.compareOfLessAndEq_of_lt_irrefl
{α : Type u_1}
[LT α]
[DecidableLT α]
[DecidableEq α]
(lt_irrefl : ∀ (x : α), ¬x < x)
:
ReflCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
theorem
Std.LawfulBEqCmp.compareOfLessAndEq_of_lt_irrefl
{α : Type u_1}
[LT α]
[DecidableLT α]
[DecidableEq α]
[BEq α]
[LawfulBEq α]
(lt_irrefl : ∀ (x : α), ¬x < x)
:
LawfulBEqCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
theorem
Std.TransCmp.compareOfLessAndEq_of_irrefl_of_trans_of_antisymm
{α : Type u_1}
[LT α]
[DecidableLT α]
[DecidableEq α]
(lt_irrefl : ∀ (x : α), ¬x < x)
(lt_trans : ∀ {x y z : α}, x < y → y < z → x < z)
(lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y)
:
TransCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
theorem
Std.TransCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm
{α : Type u_1}
[LT α]
[LE α]
[DecidableLT α]
[DecidableEq α]
(lt_irrefl : ∀ (x : α), ¬x < x)
(lt_trans : ∀ {x y z : α}, x < y → y < z → x < z)
(not_lt : ∀ {x y : α}, ¬x < y → y ≤ x)
(le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
:
TransCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
theorem
Std.LawfulLTCmp.compareOfLessAndEq_of_irrefl_of_trans_of_antisymm
{α : Type u_1}
[LT α]
[DecidableLT α]
[DecidableEq α]
(lt_irrefl : ∀ (x : α), ¬x < x)
(lt_trans : ∀ {x y z : α}, x < y → y < z → x < z)
(lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y)
:
LawfulLTCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
theorem
Std.LawfulLTCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm
{α : Type u_1}
[LT α]
[DecidableLT α]
[DecidableEq α]
[LE α]
(lt_irrefl : ∀ (x : α), ¬x < x)
(lt_trans : ∀ {x y z : α}, x < y → y < z → x < z)
(not_lt : ∀ {x y : α}, ¬x < y → y ≤ x)
(le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
:
LawfulLTCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
theorem
Std.LawfulLECmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm
{α : Type u_1}
[LT α]
[DecidableLT α]
[DecidableEq α]
[LE α]
(lt_irrefl : ∀ (x : α), ¬x < x)
(lt_trans : ∀ {x y z : α}, x < y → y < z → x < z)
(not_lt : ∀ {x y : α}, ¬x < y ↔ y ≤ x)
(le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
:
LawfulLECmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2
theorem
Std.LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm
{α : Type u_1}
[LT α]
[LE α]
[DecidableLT α]
[DecidableLE α]
[DecidableEq α]
(lt_irrefl : ∀ (x : α), ¬x < x)
(lt_trans : ∀ {x y z : α}, x < y → y < z → x < z)
(not_lt : ∀ {x y : α}, ¬x < y ↔ y ≤ x)
(le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
:
LawfulCmp fun (x1 x2 : α) => compareOfLessAndEq x1 x2