Mathlib v3 is deprecated. Go to Mathlib v4

Def locally_constant.to_continuous_map_linear_map

Modification history

2022-02-18 04:52
src/topology/continuous_function/locally_constant.lean
feat(topology/algebra): generalize `has_continuous_smul` arguments to `has_continuous_const_smul` (#11999) …
Modified locally_constant.to_continuous_map_linear_mapView on Github →
2021-09-22 07:37
src/analysis/normed_space/basic.lean
chore(*): removing unneeded imports (#9278)
Modified locally_constant.to_continuous_map_linear_mapView on Github →
2021-07-28 17:10
src/analysis/normed_space/basic.lean
feat(analysis/normed_space/basic): define inclusion `locally_constant X G → C(X, G)` as various types of bundled morphism (#8448)
Added locally_constant.to_continuous_map_linear_mapView on Github →