mathlib3

89275df0 - feat(topology/algebra/uniform_group): add characterization of total boundedness (#12808)

feat(topology/algebra/uniform_group): add characterization of total boundedness (#12808) The main result is `totally_bounded_iff_subset_finite_Union_nhds_one`. We prove it for noncommutative groups, which involves taking opposites. Add `uniform_group` instance for the opposite group. Adds several helper lemmas for * (co-)map of opposites applied to neighborhood filter * filter basis of uniformity in a uniform group in terms of neighborhood basis at identity Simplified proofs for `totally_bounded_of_forall_symm` and `totally_bounded.closure`. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>