toDual — Mathlib

English

WithBot.toDual is an equivalence between WithBot α and WithTop αᵒᵈ.

Русский

WithBot.toDual — эквивалентность между WithBot α и WithTop αᵒᵈ.

LaTeX

$$$WithBot.toDual : WithBot \alpha \simeq WithTop (\alpha^{\mathrm{op}})$$$

Lean4

/-- `WithBot.toDual` is the equivalence sending `⊥` to `⊤` and any `a : α` to `toDual a : αᵒᵈ`.
See `WithBot.toDual_top_equiv` for the related order-iso.
-/
protected def _root_.WithBot.toDual : WithBot α ≃ WithTop αᵒᵈ :=
  Equiv.refl _

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