coe_toDualTopEquiv_eq — Mathlib

English

The equality of the fun-like coercions toDualTopEquiv and the composition of duals is definitional.

Русский

Равенство соответствующих отображений задаётся по определению.

LaTeX

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

Lean4

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

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