toDualBotEquiv_coe — Mathlib

English

There is a canonical compatibility between dualization and the coe maps: applying the dual-bot equivalence to the dual of an element corresponds to taking the dual of the element viewed in WithBot.

Русский

Существует каноническое соответствие между склонением к дуальности и отображениями включения: применение эквивалента dual-bot к двойному элементу эквивалентно дуальному образу элемента, рассматриваемому в WithBot.

LaTeX

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

Lean4

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

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