# Documentation

Mathlib.Topology.ContinuousFunction.LocallyConstant

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

def LocallyConstant.toContinuousMapAddMonoidHom {X : Type u_1} {Y : Type u_2} [] [] [] [] :

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

Instances For
theorem LocallyConstant.toContinuousMapAddMonoidHom.proof_1 {X : Type u_1} {Y : Type u_2} [] [] [] [] :
0 = 0
theorem LocallyConstant.toContinuousMapAddMonoidHom.proof_2 {X : Type u_2} {Y : Type u_1} [] [] [] [] (x : ) (y : ) :
ZeroHom.toFun { toFun := LocallyConstant.toContinuousMap, map_zero' := (_ : 0 = 0) } (x + y) = ZeroHom.toFun { toFun := LocallyConstant.toContinuousMap, map_zero' := (_ : 0 = 0) } x + ZeroHom.toFun { toFun := LocallyConstant.toContinuousMap, map_zero' := (_ : 0 = 0) } y
@[simp]
theorem LocallyConstant.toContinuousMapAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [] [] [] [] (f : ) :
@[simp]
theorem LocallyConstant.toContinuousMapMonoidHom_apply {X : Type u_1} {Y : Type u_2} [] [] [] [] (f : ) :
LocallyConstant.toContinuousMapMonoidHom f = f
def LocallyConstant.toContinuousMapMonoidHom {X : Type u_1} {Y : Type u_2} [] [] [] [] :

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

Instances For
@[simp]
theorem LocallyConstant.toContinuousMapLinearMap_apply {X : Type u_1} {Y : Type u_2} [] [] (R : Type u_3) [] [] [Module R Y] [] [] (f : ) :
def LocallyConstant.toContinuousMapLinearMap {X : Type u_1} {Y : Type u_2} [] [] (R : Type u_3) [] [] [Module R Y] [] [] :

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

Instances For
@[simp]
theorem LocallyConstant.toContinuousMapAlgHom_apply {X : Type u_1} {Y : Type u_2} [] [] (R : Type u_3) [] [] [Algebra R Y] (f : ) :
def LocallyConstant.toContinuousMapAlgHom {X : Type u_1} {Y : Type u_2} [] [] (R : Type u_3) [] [] [Algebra R Y] :

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

Instances For