English
Let a and b be elements of α and f: α → β an injective function. If decision instances exist for the lifted lt, then the comparison compare (f a) (f b) equals compareOfLessAndEq a b in the lifted order.
Русский
Пусть a,b ∈ α и f: α → β — инъекция. Если существует решение для сравнения меньших и равных в поднятом порядке, то сравнение compare (f a) (f b) равно compareOfLessAndEq a b в поднятом порядке.
LaTeX
$$$\text{compare}(f a, f b) = \text{compareOfLessAndEq } a b$$$
Lean4
theorem compare_of_injective_eq_compareOfLessAndEq (a b : α) [LinearOrder β] [DecidableEq α] (f : α → β)
(inj : Injective f) [Decidable (LT.lt (self := PartialOrder.lift f inj |>.toLT) a b)] :
compare (f a) (f b) = @compareOfLessAndEq _ a b (PartialOrder.lift f inj |>.toLT) _ _ :=
by
have h := LinearOrder.compare_eq_compareOfLessAndEq (f a) (f b)
simp only [h, compareOfLessAndEq]
split_ifs <;>
try
(first
| rfl
| contradiction)
· have : ¬f a = f b := by rename_i h; exact inj.ne h
contradiction
· grind
