Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-28 17:10 32c82274

View on Github →

feat(analysis/normed_space/basic): define inclusion locally_constant X G → C(X, G) as various types of bundled morphism (#8448)

Estimated changes

Modified src/analysis/normed_space/basic.lean

added def locally_constant.to_continuous_map_alg_hom

added def locally_constant.to_continuous_map_linear_map

added def locally_constant.to_continuous_map_monoid_hom

Modified src/topology/locally_constant/algebra.lean

added theorem locally_constant.coe_algebra_map

added def locally_constant.const_monoid_hom

added def locally_constant.const_ring_hom

Modified src/topology/locally_constant/basic.lean

added theorem locally_constant.coe_const