Theorem IsClosed.vadd_right_of_isCompact

Modification history

2025-11-05 17:11
Mathlib/Topology/Algebra/Group/AddTorsor.lean
feat: generalize `IsClosed.vadd_right_of_isCompact` to proper actions (#29715) …
Deleted IsClosed.vadd_right_of_isCompactView on Github →
2025-09-15 09:41
Mathlib/Analysis/Normed/Group/AddTorsor.lean
feat: topological affine spaces (#28493) …
Modified IsClosed.vadd_right_of_isCompactView on Github →
2023-06-28 10:21
Mathlib/Analysis/Normed/Group/AddTorsor.lean
feat(Topology/Algebra/Group/Basic): product of compact set and closed set is closed (#5471) …
Added IsClosed.vadd_right_of_isCompactView on Github →