English
There is a canonical order isomorphism between WithBot(α^op) and WithTop(α) that exchanges the bottom element with the top element and identifies α with its dual. Concretely, the equivalence sends ⊥ in WithBot(α^op) to ⊤ in WithTop(α) and sends each a ∈ α^op to its dual element in α.
Русский
Существуют естественный порядковый эквивалент между WithBot(α^op) и WithTop(α), который переводит ⊥ в ⊤ и сопоставляет каждому элементу a ∈ α^op соответствующий элемент в α через дуальность.
LaTeX
$$$\\mathrm{WithBot}(\\alpha^{\\mathrm{op}}) \\cong \\mathrm{WithTop}(\\alpha),\\quad \\bot \\mapsto \\top,\\quad a^{\\mathrm{op}} \\mapsto a.$$$
Lean4
/-- `WithBot.ofDual` is the equivalence sending `⊥` to `⊤` and any `a : αᵒᵈ` to `ofDual a : α`.
See `WithBot.ofDual_top_equiv` for the related order-iso.
-/
protected def _root_.WithBot.ofDual : WithBot αᵒᵈ ≃ WithTop α :=
Equiv.refl _
