toDual — Mathlib

English

There is a natural equivalence between WithTop α and WithBot αᵒᵈ sending ⊤ to ⊥ and a to dual a.

Русский

Существует естественное эквивалентное соответствие между WithTop α и WithBot αᵒᵈ, отправляющее ⊤ в ⊥ и элемент a в двойственный a.

LaTeX

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

Lean4

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

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