Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-10 08:56 34f29db3

View on Github →

feat(topology/algebra/group): Division is an open map (#14028) A few missing lemmas about division in topological groups.

Estimated changes

modified theorem inv_closure
modified theorem is_closed.inv
added theorem is_closed_map_div_left
added theorem is_closed_map_inv
modified theorem is_compact.inv
added theorem is_open.closure_div
modified theorem is_open.closure_mul
added theorem is_open.div_closure
added theorem is_open.div_left
added theorem is_open.div_right
modified theorem is_open.inv
modified theorem is_open.mul_closure
modified theorem is_open.mul_left
modified theorem is_open.mul_right
added theorem is_open_map_div_left
added theorem is_open_map_inv
modified theorem nhds_translation_div
added theorem subset_interior_div
modified theorem subset_interior_mul
modified theorem subset_interior_mul_left
modified theorem subset_interior_mul_right