- eq_of_cmp : ∀ {a a' : α}, cmp a a' = Ordering.eq → a = a'
Proof that the equality of a compare function corresponds to propositional equality.
Instances
- eq_of_cmp : ∀ {a a' : α}, cmp a a' = Ordering.eq → a = a'
- cmp_rfl : ∀ {a : α}, cmp a a = Ordering.eq
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'
- eq_of_cmp_wrt : ∀ {a a' : α}, cmp a a' = Ordering.eq → f 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]
:
Lake.EqOfCmp α cmp
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)
:
theorem
Lake.Fin.eq_of_compare
{m : Nat}
{n : Fin m}
{n' : Fin m}
(h : compare n n' = Ordering.eq)
:
n = n'
instance
Lake.instEqOfCmpOptionCompareWith
{α : Type u_1}
{cmp : α → α → Ordering}
[Lake.EqOfCmp α cmp]
:
Lake.EqOfCmp (Option α) (Lake.Option.compareWith cmp)
instance
Lake.instLawfulCmpEqOptionCompareWith
{α : Type u_1}
{cmp : α → α → Ordering}
[Lake.LawfulCmpEq α cmp]
:
Lake.LawfulCmpEq (Option α) (Lake.Option.compareWith cmp)
instance
Lake.instEqOfCmpProdCompareWith
{α : Type u_1}
{cmpA : α → α → Ordering}
{β : Type u_2}
{cmpB : β → β → Ordering}
[Lake.EqOfCmp α cmpA]
[Lake.EqOfCmp β cmpB]
:
Lake.EqOfCmp (α × β) (Lake.Prod.compareWith cmpA cmpB)
instance
Lake.instLawfulCmpEqProdCompareWith
{α : Type u_1}
{cmpA : α → α → Ordering}
{β : Type u_2}
{cmpB : β → β → Ordering}
[Lake.LawfulCmpEq α cmpA]
[Lake.LawfulCmpEq β cmpB]
:
Lake.LawfulCmpEq (α × β) (Lake.Prod.compareWith cmpA cmpB)