The algebra morphism from locally constant functions to continuous functions. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
def
locally_constant.to_continuous_map_add_monoid_hom
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
[add_monoid Y]
[has_continuous_add Y] :
locally_constant X Y →+ C(X, Y)
The inclusion of locally-constant functions into continuous functions as an additive monoid hom.
Equations
- locally_constant.to_continuous_map_add_monoid_hom = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}
def
locally_constant.to_continuous_map_monoid_hom
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
[monoid Y]
[has_continuous_mul Y] :
locally_constant X Y →* C(X, Y)
The inclusion of locally-constant functions into continuous functions as a multiplicative monoid hom.
Equations
- locally_constant.to_continuous_map_monoid_hom = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _}
@[simp]
theorem
locally_constant.to_continuous_map_monoid_hom_apply
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
[monoid Y]
[has_continuous_mul Y]
(ᾰ : locally_constant X Y) :
@[simp]
theorem
locally_constant.to_continuous_map_add_monoid_hom_apply
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
[add_monoid Y]
[has_continuous_add Y]
(ᾰ : locally_constant X Y) :
def
locally_constant.to_continuous_map_linear_map
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
(R : Type u_3)
[semiring R]
[add_comm_monoid Y]
[module R Y]
[has_continuous_add Y]
[has_continuous_const_smul R Y] :
The inclusion of locally-constant functions into continuous functions as a linear map.
Equations
- locally_constant.to_continuous_map_linear_map R = {to_fun := coe coe_to_lift, map_add' := _, map_smul' := _}
@[simp]
theorem
locally_constant.to_continuous_map_linear_map_apply
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
(R : Type u_3)
[semiring R]
[add_comm_monoid Y]
[module R Y]
[has_continuous_add Y]
[has_continuous_const_smul R Y]
(ᾰ : locally_constant X Y) :
@[simp]
theorem
locally_constant.to_continuous_map_alg_hom_apply
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
(R : Type u_3)
[comm_semiring R]
[semiring Y]
[algebra R Y]
[topological_semiring Y]
(ᾰ : locally_constant X Y) :
def
locally_constant.to_continuous_map_alg_hom
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
(R : Type u_3)
[comm_semiring R]
[semiring Y]
[algebra R Y]
[topological_semiring Y] :
The inclusion of locally-constant functions into continuous functions as an algebra map.