English
Let α be a type with a linear order, and consider αᵒᵈ with the reversed order. Then the comparison on the dual is the reverse of the comparison on the original order: cmp(ofDual x, ofDual y) = cmp y x for all x, y in α.
Русский
Пусть α — множество с линейным порядком, возьмём αᵒᵈ с обращённым порядком. Тогда сравнение на двойственном порядке является обратным сравнению на исходном порядке: cmp(ofDual x, ofDual y) = cmp y x при любых x, y ∈ α.
LaTeX
$$$\mathrm{cmp}(\mathrm{ofDual}(x), \mathrm{ofDual}(y)) = \mathrm{cmp}(y, x)$$$
Lean4
@[simp]
theorem cmp_ofDual [LT α] [DecidableLT α] (x y : αᵒᵈ) : cmp (ofDual x) (ofDual y) = cmp y x :=
rfl
