Documentation

Mathlib.Topology.ContinuousFunction.LocallyConstant

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

source
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
    source
    theorem LocallyConstant.toContinuousMapAddMonoidHom.proof_1 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [AddMonoid Y] [ContinuousAdd Y] :
    ↑0 = 0
    source
    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) :
    { toFun := LocallyConstant.toContinuousMap, map_zero' := (_ : ↑0 = 0) }.toFun (x + y) = { toFun := LocallyConstant.toContinuousMap, map_zero' := (_ : ↑0 = 0) }.toFun x + { toFun := LocallyConstant.toContinuousMap, map_zero' := (_ : ↑0 = 0) }.toFun y
    source
    @[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
    source
    @[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
    source
    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
      source
      @[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
      source
      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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[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
        source
        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
        • One or more equations did not get rendered due to their size.
        Instances For