The algebra morphism from locally constant functions to continuous functions.

def LocallyConstant.toContinuousMapMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Monoid Y] [ContinuousMul Y] : LocallyConstant X Y →* C(X, Y)

The inclusion of locally-constant functions into continuous functions as a multiplicative monoid hom.

def LocallyConstant.toContinuousMapAddMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [AddMonoid Y] [ContinuousAdd Y] : LocallyConstant X Y →+ C(X, Y)

The inclusion of locally-constant functions into continuous functions as an additive monoid hom.

@[simp]

theorem LocallyConstant.toContinuousMapMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Monoid Y] [ContinuousMul Y] (f : LocallyConstant X Y) : toContinuousMapMonoidHom f = ↑f

@[simp]

theorem LocallyConstant.toContinuousMapAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [AddMonoid Y] [ContinuousAdd Y] (f : LocallyConstant X Y) : toContinuousMapAddMonoidHom f = ↑f

def LocallyConstant.toContinuousMapLinearMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [Semiring R] [AddCommMonoid Y] [Module R Y] [ContinuousAdd Y] [ContinuousConstSMul R Y] : LocallyConstant X Y →ₗ[R] C(X, Y)

The inclusion of locally-constant functions into continuous functions as a linear map.

@[simp]

theorem LocallyConstant.toContinuousMapLinearMap_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [Semiring R] [AddCommMonoid Y] [Module R Y] [ContinuousAdd Y] [ContinuousConstSMul R Y] (f : LocallyConstant X Y) : (toContinuousMapLinearMap R) f = ↑f

def LocallyConstant.toContinuousMapAlgHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [CommSemiring R] [Semiring Y] [Algebra R Y] [IsTopologicalSemiring Y] : LocallyConstant X Y →ₐ[R] C(X, Y)

The inclusion of locally-constant functions into continuous functions as an algebra map.

@[simp]

theorem LocallyConstant.toContinuousMapAlgHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [CommSemiring R] [Semiring Y] [Algebra R Y] [IsTopologicalSemiring Y] (f : LocallyConstant X Y) : (toContinuousMapAlgHom R) f = ↑f