coe_toDualBotEquiv — Mathlib

English

The canonical map from WithTop αᵒᵈ to (WithBot α)ᵒᵈ is equal to the composition of toDual with WithTop.ofDual.

Русский

Каноническое отображение From WithTop αᵒᵈ к (WithBot α)ᵒᵈ равно композиции toDual ∘ WithTop.ofDual.

LaTeX

$$$(WithTop.toDualBotEquiv) = (toDual \\circ WithTop.ofDual)$$$

Lean4

theorem coe_toDualBotEquiv [LE α] : (WithTop.toDualBotEquiv : WithTop αᵒᵈ → (WithBot α)ᵒᵈ) = toDual ∘ WithTop.ofDual :=
  funext fun _ => rfl

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