Commit 2025-11-05 17:11 68b37c8b

feat: generalize IsClosed.vadd_right_of_isCompact to proper actions (#29715) I realized a few weeks after adding them to Mathlib that the more conceptual approach for lemmas of the form "s • t is closed when one of s and t is closed and the other is compact" is that of proper maps and proper actions. This PR switches to this approach. More precisely:

• I refactored the proof IsClosed.smul_left_of_isCompact in terms of properness. The proof is essentially the same length, but conceptually simpler.
• More importantly, I generalize IsClosed.vadd_right_of_isCompact from topological torsors to proper actions. Note that I do not assume separation, which creates some troubles as compact sets are not closed...