ofDual — Mathlib

English

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

Русский

WithTop.ofDual образует эквивалентность между WithTop αᵒᵈ и WithBot α.

LaTeX

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

Lean4

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

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