# The algebra morphism from locally constant functions to continuous functions. #

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.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

theorem
LocallyConstant.toContinuousMapAddMonoidHom.proof_1
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[AddMonoid Y]
[ContinuousAdd Y]
:

↑0 = 0

theorem
LocallyConstant.toContinuousMapAddMonoidHom.proof_2
{X : Type u_2}
{Y : Type u_1}
[TopologicalSpace X]
[TopologicalSpace Y]
[AddMonoid Y]
[ContinuousAdd Y]
(x : LocallyConstant X Y)
(y : LocallyConstant X Y)
:

@[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)
:

LocallyConstant.toContinuousMapAddMonoidHom f = ↑f

@[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)
:

LocallyConstant.toContinuousMapMonoidHom f = ↑f

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.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

@[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)
:

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]
:

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

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

@[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]
[TopologicalSemiring Y]
(f : LocallyConstant X Y)
:

(LocallyConstant.toContinuousMapAlgHom 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]
[TopologicalSemiring Y]
:

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

## Equations

- One or more equations did not get rendered due to their size.