Commit 2024-10-07 17:59 6fc3b64c

View on Github →

chore(Topology): rename some prod_map/prod to prodMap (#17472) Also

  • replace some proofs by fun_prop
  • use Prod.map instead of an inline lambda in some lemmas
  • fix to_additive name for ContinuousAddMonoidHom.prod and ContinuousAddMonoidHom.prodMap (were sum and sum_map).

Estimated changes

added theorem Continuous.prodMap
deleted theorem Continuous.prod_map
added theorem ContinuousAt.prodMap'
added theorem ContinuousAt.prodMap
deleted theorem ContinuousAt.prod_map'
deleted theorem ContinuousAt.prod_map
added theorem DenseRange.prodMap
deleted theorem DenseRange.prod_map
added theorem Embedding.prodMap
deleted theorem Embedding.prod_map
added theorem Inducing.prodMap
deleted theorem Inducing.prod_map
added theorem IsProperMap.prodMap
deleted theorem IsProperMap.prod_map