mathlib documentation

topology.continuous_function.locally_constant

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

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

Equations

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

Equations

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

Equations

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

Equations