Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-22 10:50 68efb10c

View on Github →

refactor(topology/*): Hom classes for continuous maps/homs (#11909) Add

  • continuous_map_class
  • bounded_continuous_map_class
  • continuous_monoid_hom_class
  • continuous_add_monoid_hom_class
  • continuous_map.homotopy_class to follow the fun_like design. Deprecate lemmas accordingly. Also rename a few fields to match the convention in the rest of the library.

Estimated changes

modified theorem prime_spectrum.comap_id
modified structure continuous_monoid_hom
modified theorem continuous_map.coe_const'
modified theorem continuous_map.coe_mul
modified theorem continuous_map.coe_one
modified theorem continuous_map.one_comp
added theorem continuous_map.coe_id
modified theorem continuous_map.comp_apply
deleted theorem continuous_map.comp_coe
modified theorem continuous_map.comp_id
modified def continuous_map.const
modified theorem continuous_map.const_apply
deleted theorem continuous_map.const_coe
modified theorem continuous_map.ext
deleted theorem continuous_map.ext_iff
deleted def continuous_map.id
modified theorem continuous_map.id_apply
deleted theorem continuous_map.id_coe
modified theorem continuous_map.id_comp
modified structure continuous_map
added theorem map_continuous_at
modified theorem continuous_map.homotopy.ext