English
Two LinearOrders on α are equal if their induced PartialOrders are equal.
Русский
Два линейных порядка на α равны, если порожденные ими частичные порядки равны.
LaTeX
$$$ \forall A,B:\text{LinearOrder}(\alpha),\ (toPartialOrder\,A = toPartialOrder\,B) \rightarrow A = B $$$
Lean4
@[ext]
theorem toPartialOrder_injective : Function.Injective (@LinearOrder.toPartialOrder α) := fun
| { le := A_le, lt := A_lt, toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq,
toDecidableLT := A_decidableLT
min := A_min, max := A_max, min_def := A_min_def, max_def := A_max_def, compare := A_compare,
compare_eq_compareOfLessAndEq := A_compare_canonical, .. },
{ le := B_le, lt := B_lt, toDecidableLE := B_decidableLE, toDecidableEq := B_decidableEq,
toDecidableLT := B_decidableLT
min := B_min, max := B_max, min_def := B_min_def, max_def := B_max_def, compare := B_compare,
compare_eq_compareOfLessAndEq := B_compare_canonical, .. } =>
by
rintro ⟨⟩
obtain rfl : A_decidableLE = B_decidableLE := Subsingleton.elim _ _
obtain rfl : A_decidableEq = B_decidableEq := Subsingleton.elim _ _
obtain rfl : A_decidableLT = B_decidableLT := Subsingleton.elim _ _
have : A_min = B_min := by
funext a b
exact (A_min_def _ _).trans (B_min_def _ _).symm
cases this
have : A_max = B_max := by
funext a b
exact (A_max_def _ _).trans (B_max_def _ _).symm
cases this
have : A_compare = B_compare := by
funext a b
exact (A_compare_canonical _ _).trans (B_compare_canonical _ _).symm
congr
