Commit 2022-04-01 12:39 89275df0

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.