# mathlibdocumentation

topology.continuous_function.locally_constant

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

def locally_constant.to_continuous_map_add_monoid_hom {X : Type u_1} {Y : Type u_2} [add_monoid Y]  :

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

Equations
def locally_constant.to_continuous_map_monoid_hom {X : Type u_1} {Y : Type u_2} [monoid Y]  :

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

Equations
@[simp]
theorem locally_constant.to_continuous_map_monoid_hom_apply {X : Type u_1} {Y : Type u_2} [monoid Y] (ᾰ : Y) :
@[simp]
theorem locally_constant.to_continuous_map_add_monoid_hom_apply {X : Type u_1} {Y : Type u_2} [add_monoid Y] (ᾰ : Y) :
def locally_constant.to_continuous_map_linear_map {X : Type u_1} {Y : Type u_2} (R : Type u_3) [semiring R] [ Y]  :

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

Equations
@[simp]
theorem locally_constant.to_continuous_map_linear_map_apply {X : Type u_1} {Y : Type u_2} (R : Type u_3) [semiring R] [ Y] (ᾰ : Y) :
@[simp]
theorem locally_constant.to_continuous_map_alg_hom_apply {X : Type u_1} {Y : Type u_2} (R : Type u_3) [semiring Y] [ Y] (ᾰ : Y) :
def locally_constant.to_continuous_map_alg_hom {X : Type u_1} {Y : Type u_2} (R : Type u_3) [semiring Y] [ Y]  :

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

Equations