English
LocallyConstant comap as a linear map: for a ContinuousMap f, comap f induces a linear map comapₗ from LocallyConstant Y Z to LocallyConstant X Z commuting with addition and scalar multiplication.
Русский
LocallyConstant comap как линейное отображение: для непрерывного отображения f моноид-композиция образует линейное отображение comapₗ, сохраняющее сложение и умножение на скаляр.
LaTeX
$$$\operatorname{comap}_{\ell}(f): \operatorname{LocallyConstant}(Y,Z) \to_{\mathrm{Linear}} \operatorname{LocallyConstant}(X,Z)$$$
Lean4
/-- `LocallyConstant.comap` as a linear map. -/
@[simps!]
def comapₗ (R : Type*) [Semiring R] [AddCommMonoid Z] [Module R Z] (f : C(X, Y)) :
LocallyConstant Y Z →ₗ[R] LocallyConstant X Z
where
toFun := comap f
map_add' := map_add (comapAddMonoidHom f)
map_smul' _ _ := rfl
