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

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

• eq_of_cmp : ∀ {a a' : α}, cmp a a' = Ordering.eq → a = a'

class Lake.LawfulCmpEq (α : Type u) (cmp : α → α → Ordering) extends Lake.EqOfCmp α cmp : Prop

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

• eq_of_cmp : ∀ {a a' : α}, cmp a a' = Ordering.eq → a = a'
• cmp_rfl : ∀ {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) : Prop

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.eq → f a = f a'

instance Lake.instEqOfCmpWrtOfEqOfCmp {α : Type u_1} {cmp : α → α → Ordering} {β✝ : Type u_2} {f : α → β✝} [Lake.EqOfCmp α cmp] : Lake.EqOfCmpWrt α f cmp

Equations

• ⋯ = ⋯

theorem Lake.eq_of_compareOfLessAndEq {α : Type u_1} [LT α] [DecidableEq α] {a a' : α} [Decidable (a < a')] (h : compareOfLessAndEq a a' = Ordering.eq) : a = a'

theorem Lake.compareOfLessAndEq_rfl {α : Type u_1} [LT α] [DecidableEq α] {a : α} [Decidable (a < a)] (lt_irrefl : ¬a < a) : compareOfLessAndEq a a = Ordering.eq

instance Lake.instLawfulCmpEqNatCompare : Lake.LawfulCmpEq Nat compare

Equations

• Lake.instLawfulCmpEqNatCompare = ⋯

instance Lake.instLawfulCmpEqUInt64Compare : Lake.LawfulCmpEq UInt64 compare

Equations

• Lake.instLawfulCmpEqUInt64Compare = ⋯

instance Lake.instLawfulCmpEqStringCompare : Lake.LawfulCmpEq String compare

Equations

• Lake.instLawfulCmpEqStringCompare = ⋯