# Documentation

Lake.Util.Compare

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

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

Instances
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.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) :
• eq_of_cmp_wrt : ∀ {a a' : α}, cmp a a' = Ordering.eqf a = f a'

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

Instances
instance Lake.instEqOfCmpWrtType {α : Type u_1} {cmp : ααOrdering} :
Lake.EqOfCmpWrt α (fun x => α) cmp
instance Lake.instEqOfCmpWrt {α : Type u_1} {cmp : ααOrdering} :
{β : Type u_2} → {f : αβ} → [inst : Lake.EqOfCmp α cmp] → Lake.EqOfCmpWrt α f cmp
instance Lake.instEqOfCmp {α : Type u_1} {cmp : ααOrdering} [Lake.EqOfCmpWrt α (fun a => a) 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'
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
Instances For
instance Lake.instEqOfCmpOptionCompareWith {α : Type u_1} {cmp : ααOrdering} [Lake.EqOfCmp α cmp] :
instance Lake.instLawfulCmpEqOptionCompareWith {α : Type u_1} {cmp : ααOrdering} [Lake.LawfulCmpEq α cmp] :
def Lake.Prod.compareWith {α : Type u_1} {β : Type u_2} (cmpA : ααOrdering) (cmpB : ββOrdering) :
α × βα × βOrdering
Instances For
instance Lake.instEqOfCmpProdCompareWith {α : Type u_1} {cmpA : ααOrdering} {β : Type u_2} {cmpB : ββOrdering} [Lake.EqOfCmp α cmpA] [Lake.EqOfCmp β cmpB] :
instance Lake.instLawfulCmpEqProdCompareWith {α : Type u_1} {cmpA : ααOrdering} {β : Type u_2} {cmpB : ββOrdering} [Lake.LawfulCmpEq α cmpA] [Lake.LawfulCmpEq β cmpB] :