toDual_apply_coe — Mathlib

English

For any a ∈ α, the dual of its embedding into WithTop(α) equals the dual of a in the base dual.

Русский

Для любого a ∈ α дуальное отображение его в WithTop(α) совпадает с дуальным отображением a в основе дуальности.

LaTeX

$$$\\forall a\\in \\alpha:\\; \\mathrm{toDual}(a\\,\\text{embedded}) = \\mathrm{toDual}(a).$$$

Lean4

@[simp]
theorem toDual_apply_coe (a : α) : WithTop.toDual (a : WithTop α) = toDual a :=
  rfl

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