Documentation

Mathlib.Topology.ContinuousFunction.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' := }
Instances For
    @[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' := }
    Instances For

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

      Equations
      Instances For

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

        Equations
        Instances For