English
Let α be a type with a strict order. In the augmented order on WithTop of the opposite order on α, the embedding of x into WithTop reverses the order: for all x, y in WithTop(α^op), WithTop.ofDual x < WithTop.ofDual y if and only if y < x.
Русский
Пусть α - множество с жестким порядком. В дополненном порядке на WithTop от противоположного порядка на α внедрение ofDual разворачивает порядок: для любых x, y ∈ WithTop(α^op) верно, что WithTop.ofDual x < WithTop.ofDual y тогда и только если y < x.
LaTeX
$$$\\\\forall x,y \in WithTop(\\\\alpha^{\\\\mathrm{op}}),\\\\ WithTop.ofDual x < WithTop.ofDual y \\\\iff y < x.$$$
Lean4
@[simp]
theorem ofDual_lt_ofDual_iff {x y : WithTop αᵒᵈ} : WithTop.ofDual x < WithTop.ofDual y ↔ y < x := by
cases x <;> cases y <;> simp
