English
To show that f: α → β and g: β → α form an order isomorphism between linear orders, it suffices that for all a ∈ α and b ∈ β, cmp a (g b) = cmp (f a) b.
Русский
Чтобы показать, что f: α → β и g: β → α образуют порядковый изоморфизм между линейными порядками, достаточно, чтобы для всех a ∈ α и b ∈ β выполнялось cmp a (g b) = cmp (f a) b.
LaTeX
$$$\forall a:\alpha\,\forall b:\beta,\operatorname{cmp}(a, g(b)) = \operatorname{cmp}(f(a), b) \Rightarrow \alpha \simeq_o \beta$$$
Lean4
/-- To show that `f : α → β`, `g : β → α` make up an order isomorphism of linear orders,
it suffices to prove `cmp a (g b) = cmp (f a) b`. -/
def ofCmpEqCmp {α β} [LinearOrder α] [LinearOrder β] (f : α → β) (g : β → α)
(h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b) : α ≃o β :=
have gf : ∀ a : α, a = g (f a) := by
intro
rw [← cmp_eq_eq_iff, h, cmp_self_eq_eq]
{ toFun := f, invFun := g, left_inv := fun a => (gf a).symm,
right_inv := by
intro
rw [← cmp_eq_eq_iff, ← h, cmp_self_eq_eq],
map_rel_iff' := by
intro a b
apply le_iff_le_of_cmp_eq_cmp
convert (h a (f b)).symm
apply gf }
