Commit 2023-10-07 08:18 b097a5ad

View on Github →

feat: open mapping theorem for surjective morphisms between locally compact groups (#7356)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

added theorem MulAction.compHom_smul_def

added theorem MulAction.isPretransitive_compHom

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

added theorem exists_closed_nhds_one_inv_eq_mul_subset

Created Mathlib/Topology/Algebra/Group/OpenMapping.lean

added theorem MonoidHom.isOpenMap_of_sigmaCompact

added theorem isOpenMap_smul_of_sigmaCompact

added theorem smul_singleton_mem_nhds_of_sigmaCompact

Modified Mathlib/Topology/Algebra/MulAction.lean

added theorem MulAction.continuousSMul_compHom