Documentation

Mathlib.Topology.ContinuousMap.LocallyConstant

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

source
🔸 coverage
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.

Instances For
    source
    🔸 coverage
    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.

    Instances For
      source
      📐 coverage
      @[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) :
      toContinuousMapMonoidHom f = ↑f
      source
      📐 coverage
      @[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) :
      toContinuousMapAddMonoidHom f = ↑f
      source
      🔸 coverage
      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.

      Instances For
        source
        📐 coverage
        @[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) :
        (toContinuousMapLinearMap R) f = ↑f
        source
        📐 coverage
        @[simp]
        theorem LocallyConstant.toAddMonoidHom_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] :
        (toContinuousMapLinearMap R).toAddMonoidHom = toContinuousMapAddMonoidHom
        source
        🔸 coverage
        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] [IsTopologicalSemiring Y] :
        LocallyConstant X Y →ₐ[R] C(X, Y)

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

        Instances For
          source
          📐 coverage
          @[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] [IsTopologicalSemiring Y] (f : LocallyConstant X Y) :
          (toContinuousMapAlgHom R) f = ↑f
          source
          📐 coverage
          @[simp]
          theorem LocallyConstant.toLinearMap_toContinuousMapAlgHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [CommSemiring R] [Semiring Y] [Algebra R Y] [IsTopologicalSemiring Y] :
          (toContinuousMapAlgHom R).toLinearMap = toContinuousMapLinearMap R
          source
          📐 coverage
          theorem LocallyConstant.separatesPoints_range_toContinuousMapAlgHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [CommSemiring R] [TotallySeparatedSpace X] [Semiring Y] [Algebra R Y] [IsTopologicalSemiring Y] [Nontrivial Y] :
          (toContinuousMapAlgHom R).range.SeparatesPoints