compare_val — Mathlib

English

The compare operation on Units α matches the compare on α when applied to the underlying values: compare a.val b.val = compare a b.

Русский

Операция сравнения на единицах совпадает с операцией сравнения на α при применении к значениям: compare a.val b.val = compare a b.

LaTeX

$$$\\forall {a,b \\in \\mathrm{Units}(\\alpha)},\\ \\mathrm{compare}_{\\alpha}(a.\\mathrm{val}, b.\\mathrm{val}) = \\mathrm{compare}_{\\mathrm{Units}}(a,b)$$$

Lean4

@[to_additive]
theorem compare_val [Monoid α] [Ord α] (a b : αˣ) : compare a.val b.val = compare a b :=
  rfl

Похожие утверждения