Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-24 13:34 9dc3b4d6

View on Github →

feat(topology/algebra/group): continuous div lemmas (#9905)

  • From the sphere eversion project
  • There were already some lemmas about sub, now they also have multiplicative versions
  • Add more lemmas about div being continuous
  • Add continuous_at.inv
  • Rename nhds_translation -> nhds_translation_sub.

Estimated changes

added theorem continuous.div'
deleted theorem continuous.sub
added theorem continuous_at.div'
added theorem continuous_at.inv
added theorem continuous_div_left'
added theorem continuous_div_right'
added theorem continuous_on.div'
deleted theorem continuous_on.sub
deleted theorem continuous_within_at.sub
added theorem filter.tendsto.div'
deleted theorem filter.tendsto.sub
deleted theorem nhds_translation
added theorem nhds_translation_div