The algebra morphism from locally constant functions to continuous functions.

theorem LocallyConstant.toContinuousMapAddMonoidHom.proof_2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [AddMonoid Y] [ContinuousAdd Y] (x : LocallyConstant X Y) (y : LocallyConstant X Y) : { toFun := LocallyConstant.toContinuousMap, map_zero' := ⋯ }.toFun (x + y) = { toFun := LocallyConstant.toContinuousMap, map_zero' := ⋯ }.toFun x + { toFun := LocallyConstant.toContinuousMap, map_zero' := ⋯ }.toFun y

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

• LocallyConstant.toContinuousMapAddMonoidHom = { toFun := LocallyConstant.toContinuousMap, map_zero' := ⋯, map_add' := ⋯ }

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

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

• LocallyConstant.toContinuousMapMonoidHom = { toFun := LocallyConstant.toContinuousMap, map_one' := ⋯, map_mul' := ⋯ }

@[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) : (LocallyConstant.toContinuousMapLinearMap R) 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.

Equations

• LocallyConstant.toContinuousMapLinearMap R = { toFun := LocallyConstant.toContinuousMap, map_add' := ⋯, map_smul' := ⋯ }

@[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] : LocallyConstant X Y →ₐ[R] C(X, Y)

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

Equations

• LocallyConstant.toContinuousMapAlgHom R = { toFun := LocallyConstant.toContinuousMap, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }