Proof that the equality of a compare function corresponds to propositional equality.
- eq_of_cmp : ∀ {a a' : α}, cmp a a' = Ordering.eq → a = a'
Instances
theorem
Lake.EqOfCmp.eq_of_cmp
{α : Type u}
{cmp : α → α → Ordering}
[self : Lake.EqOfCmp α cmp]
{a : α}
{a' : α}
:
cmp a a' = Ordering.eq → a = a'
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.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'
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'
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.eq → f a = f a'
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 := ⋯ }
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)
: