# Documentation

## Lake.Util.Compare

class Lake.EqOfCmp (α : Type u) (cmp : ααOrdering) :

Proof that the equality of a compare function corresponds to propositional equality.

Instances
theorem Lake.EqOfCmp.eq_of_cmp {α : Type u} {cmp : ααOrdering} [self : Lake.EqOfCmp α cmp] {a : α} {a' : α} :
cmp a a' = Ordering.eqa = a'
class Lake.LawfulCmpEq (α : Type u) (cmp : ααOrdering) extends :

Proof that the equality of a compare function corresponds to propositional equality and vice versa.

Instances
@[simp]
theorem Lake.LawfulCmpEq.cmp_rfl {α : Type u} {cmp : ααOrdering} [self : Lake.LawfulCmpEq α cmp] {a : α} :
cmp a a = Ordering.eq
@[simp]
theorem Lake.cmp_iff_eq {α : Type u_1} {cmp : ααOrdering} {a : α} {a' : α} [Lake.LawfulCmpEq α cmp] :
cmp a a' = Ordering.eq a = a'
class Lake.EqOfCmpWrt (α : Type u) {β : Type v} (f : αβ) (cmp : ααOrdering) :

Proof that the equality of a compare function corresponds to propositional equality with respect to a given function.

• eq_of_cmp_wrt : ∀ {a a' : α}, cmp a a' = Ordering.eqf a = f a'
Instances
theorem Lake.EqOfCmpWrt.eq_of_cmp_wrt {α : Type u} {β : Type v} {f : αβ} {cmp : ααOrdering} [self : Lake.EqOfCmpWrt α f cmp] {a : α} {a' : α} :
cmp a a' = Ordering.eqf a = f a'
instance Lake.instEqOfCmpWrt {α : Type u_1} {cmp : ααOrdering} :
Lake.EqOfCmpWrt α (fun (x : α) => α) cmp
Equations
• Lake.instEqOfCmpWrt = { eq_of_cmp_wrt := }
instance Lake.instEqOfCmpWrtOfEqOfCmp {α : Type u_1} {cmp : ααOrdering} :
{β : Type u_2} → {f : αβ} → [inst : Lake.EqOfCmp α cmp] → Lake.EqOfCmpWrt α f cmp
Equations
• Lake.instEqOfCmpWrtOfEqOfCmp = { eq_of_cmp_wrt := }
instance Lake.instEqOfCmpOfEqOfCmpWrt {α : Type u_1} {cmp : ααOrdering} [Lake.EqOfCmpWrt α (fun (a : α) => a) cmp] :
Equations
• Lake.instEqOfCmpOfEqOfCmpWrt = { eq_of_cmp := }
theorem Lake.eq_of_compareOfLessAndEq {α : Type u_1} [LT α] [] {a : α} {a' : α} [Decidable (a < a')] (h : ) :
a = a'
theorem Lake.compareOfLessAndEq_rfl {α : Type u_1} [LT α] [] {a : α} [Decidable (a < a)] (lt_irrefl : ¬a < a) :
theorem Lake.Fin.eq_of_compare {m : Nat} {n : Fin m} {n' : Fin m} (h : compare n n' = Ordering.eq) :
n = n'
Equations
• Lake.instLawfulCmpEqFinCompare =
theorem Lake.List.lt_irrefl {α : Type u_1} [LT α] (irrefl_α : ∀ (a : α), ¬a < a) (a : List α) :
¬a < a
@[simp]
theorem Lake.String.lt_irrefl (s : String) :
¬s < s
@[macro_inline]
def Lake.Option.compareWith {α : Type u_1} (cmp : ααOrdering) :
Ordering
Equations
Instances For
instance Lake.instEqOfCmpOptionCompareWith {α : Type u_1} {cmp : ααOrdering} [Lake.EqOfCmp α cmp] :
Equations
• Lake.instEqOfCmpOptionCompareWith = { eq_of_cmp := }
instance Lake.instLawfulCmpEqOptionCompareWith {α : Type u_1} {cmp : ααOrdering} [Lake.LawfulCmpEq α cmp] :
Equations
• Lake.instLawfulCmpEqOptionCompareWith =
def Lake.Prod.compareWith {α : Type u_1} {β : Type u_2} (cmpA : ααOrdering) (cmpB : ββOrdering) :
α × βα × βOrdering
Equations
Instances For
instance Lake.instEqOfCmpProdCompareWith {α : Type u_1} {cmpA : ααOrdering} {β : Type u_2} {cmpB : ββOrdering} [Lake.EqOfCmp α cmpA] [Lake.EqOfCmp β cmpB] :
Equations
• Lake.instEqOfCmpProdCompareWith = { eq_of_cmp := }
instance Lake.instLawfulCmpEqProdCompareWith {α : Type u_1} {cmpA : ααOrdering} {β : Type u_2} {cmpB : ββOrdering} [Lake.LawfulCmpEq α cmpA] [Lake.LawfulCmpEq β cmpB] :
Equations
• Lake.instLawfulCmpEqProdCompareWith =