coe_coe — Mathlib

English

The coercion from the character space to WeakDual behaves as expected: the evaluation equals the underlying function.

Русский

Сведение из пространства характеристик к слабому двойственному пространству согласовано: оценка равна базовой функции.

LaTeX

$$$\\\\mathrm{coe}_{(φ}: (characterSpace 𝕜 A) \\to (A \\to 𝕜)) = φ$$$

Lean4

/-- This has to come after `WeakDual.CharacterSpace.instFunLike`, otherwise the right-hand side
gets coerced via `Subtype.val` instead of directly via `DFunLike`. -/
@[simp, norm_cast]
protected theorem coe_coe (φ : characterSpace 𝕜 A) : ⇑(φ : WeakDual 𝕜 A) = (φ : A → 𝕜) :=
  rfl

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