toContinuousMapLinearMap — Mathlib

English

The forgetful linear map is 𝕜-linear: it preserves addition and scalar multiplication.

Русский

Забывающее отображение является 𝕜-линейным: сохраняет сложение и скалярное умножение.

LaTeX

$$$\\text{toContinuousMapLinearMap}$ is linear over 𝕜$$

Lean4

/-- The linear map forgetting that a bounded continuous function is bounded. -/
@[simps]
def toContinuousMapLinearMap : (α →ᵇ β) →ₗ[𝕜] C(α, β)
    where
  toFun := toContinuousMap
  map_smul' _ _ := rfl
  map_add' _ _ := rfl

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