toDualBotEquiv_symm_coe — Mathlib

English

The inverse of the dual-bot equivalence matches the dual embedding on WithTop/WithBot contexts.

Русский

Обратное к эквивалентности dual-bot соответствует двойственному вложению в контекстах WithTop/WithBot.

LaTeX

$$$\mathrm{WithTop.toDualBotEquiv}^{-1}(\mathrm{toDual}(a : \mathrm{WithBot}\, \alpha)) = \uparrow(\mathrm{toDual}a)$$$

Lean4

@[simp]
theorem toDualBotEquiv_symm_coe [LE α] (a : α) : WithTop.toDualBotEquiv.symm (toDual (a : WithBot α)) = ↑(toDual a) :=
  rfl

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