Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-11 21:16 665cc13c

View on Github →

chore(topology/algebra/group): review (#4570)

  • Ensure that we don't use [topological_group G] when it suffices to ask for, e.g., [has_continuous_mul G].
  • Introduce [has_continuous_sub], add an instance for nnreal.

Estimated changes

modified theorem continuous.inv
modified theorem continuous.sub
deleted theorem continuous_at.inv
added theorem continuous_at_inv
deleted theorem continuous_inv
modified theorem continuous_on.inv
modified theorem continuous_on.sub
modified theorem continuous_on_inv
deleted theorem continuous_sub
modified theorem continuous_within_at.inv
modified theorem exists_nhds_split_inv
modified theorem filter.tendsto.inv
modified theorem filter.tendsto.sub
modified theorem is_closed_map_mul_left
modified theorem is_closed_map_mul_right
added theorem is_open.mul_left
added theorem is_open.mul_right
modified theorem is_open_map_mul_left
modified theorem is_open_map_mul_right
deleted theorem is_open_mul_left
deleted theorem is_open_mul_right
modified theorem nhds_one_symm
modified theorem nhds_translation
modified theorem nhds_translation_mul_inv
modified theorem tendsto_inv
deleted theorem nnreal.continuous.sub
deleted theorem nnreal.continuous_sub