Documentation

Mathlib.Topology.ContinuousMap.LocallyConstant

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

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

Equations
  • LocallyConstant.toContinuousMapAddMonoidHom = { toFun := LocallyConstant.toContinuousMap, map_zero' := , map_add' := }
@[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

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

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

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

Equations

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

Equations