toContinuousMapStarₐ — Mathlib

English

The coercion toContinuousMapStar aligns with the underlying function, i.e., the coe of star f equals the function f.

Русский

Сведение к отображению звезды согласуется с базовой функцией: коe звезды f равно f как функция.

LaTeX

$$$$ \text{coe}(\text{star } f) = f.$$$$

Lean4

/-- The ⋆-algebra-homomorphism forgetting that a bounded continuous function is bounded. -/
@[simps!]
def toContinuousMapStarₐ : (α →ᵇ β) →⋆ₐ[𝕜] C(α, β) :=
  { toContinuousMapₐ 𝕜 with map_star' _ := rfl }

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