toContinuousMapLinearMap — Mathlib

English

The inclusion of locally constant functions into continuous functions is linear over a ring R. It defines an R-linear map into C(X, Y).

Русский

Включение локально константных функций в непрерывные функции является линейным относительно кольца R, образуя линейный отображение.

LaTeX

$$\$LocallyConstant\\, X\\, Y \\to_L[R] C(X, Y)\$ is the inclusion map, i.e. a linear map preserving addition and scalar multiplication.$$

Lean4

/-- The inclusion of locally-constant functions into continuous functions as a linear map. -/
@[simps]
def toContinuousMapLinearMap (R : Type*) [Semiring R] [AddCommMonoid Y] [Module R Y] [ContinuousAdd Y]
    [ContinuousConstSMul R Y] : LocallyConstant X Y →ₗ[R] C(X, Y)
    where
  toFun := (↑)
  map_add' x
    y := by
    ext
    simp
  map_smul' x
    y := by
    ext
    simp

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