Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-15 13:39 29675ad2

View on Github →

refactor(analysis/topology/topological_structures): use to_additive to derive topological_add_monoid and topological_add_group

Estimated changes

deleted theorem continuous_inv'
deleted theorem continuous_inv
deleted theorem is_open_add_translate
added theorem is_open_coinduced
modified theorem is_open_map.of_inverse
deleted theorem is_open_map_iff_nhds_sets
added theorem is_open_map_mul_left
added theorem is_open_map_mul_right
deleted theorem is_open_translate
deleted theorem quotient_ring.is_open_map
deleted theorem quotient_ring.open_coe
deleted theorem continuous_add'
deleted theorem continuous_add
deleted theorem continuous_finset_sum
added theorem continuous_inv'
added theorem continuous_inv
deleted theorem continuous_list_sum
deleted theorem continuous_multiset_sum
deleted theorem continuous_neg'
deleted theorem continuous_neg
deleted theorem exists_nhds_half
deleted theorem exists_nhds_quarter
added theorem exists_nhds_split4
added theorem exists_nhds_split
added theorem nhds_one_symm
deleted theorem nhds_zero_symm
deleted theorem tendsto_add'
deleted theorem tendsto_add
deleted theorem tendsto_finset_sum
added theorem tendsto_inv
deleted theorem tendsto_list_sum
deleted theorem tendsto_multiset_sum
deleted theorem tendsto_neg