feat(measure_theory/group/fundamental_domain): a large set contains 2 pts of the same orbit (#17293)
feat(measure_theory/group/fundamental_domain): a large set contains 2 pts of the same orbit (#17293)

Motivated by #2819 





leanprover-community/mathlib,leanprover-community/mathlib