Commit 2026-03-24 19:17 9ec3a36f

View on Github →

feat(Topology/Algebra/ProperAction): Fiberwise criterion for ProperSMul (#36904) Criterion for properness of transitive group actions in terms of properness of orbit maps.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

added theorem properlyDiscontinuousSMul_iff

Modified Mathlib/Topology/Algebra/ProperAction/Basic.lean

added theorem MulAction.properSMul_of_proper_orbitMap

added theorem ProperSMul.isCompact_setOf_inter_nonempty

Created Mathlib/Topology/Algebra/ProperAction/CompactlyGenerated.lean

added theorem MulAction.properSMul_iff_isCompact_setOf_inter_nonempty

added theorem properlyDiscontinuousSMul_iff_properSMul

Deleted Mathlib/Topology/Algebra/ProperAction/ProperlyDiscontinuous.lean

deleted theorem properlyDiscontinuousSMul_iff_properSMul