mathlib3 documentation

topology.continuous_function.locally_constant

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.

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