constₗ — Mathlib

English

The constant map from Y to LocallyConstant(X,Y) sending y to the constant function X → Y is a linear map, i.e., a map from Y into LocallyConstant(X,Y) which is linear in the module structure.

Русский

Постоянное отображение из Y в LocallyConstant(X,Y), отправляющее y на константную функцию X → Y, является линейным отображением.

LaTeX

$$$\\mathrm{const}_{\\ell} : Y \\to_{R} \\operatorname{LocallyConstant}(X,Y), \\quad (\\mathrm{const}_{\\ell}(y))(x) = y$$$

Lean4

/-- `LocallyConstant.const` as a linear map. -/
@[simps!]
def constₗ (R : Type*) [Semiring R] [AddCommMonoid Y] [Module R Y] : Y →ₗ[R] LocallyConstant X Y
    where
  toFun := const X
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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