Theorems · Theorem · manifolds

IsClosed.smul_right_of_isCompact

∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ProperSMul G X] {s : Set G} {t : Set X}, IsClosed s → IsCompact t → IsClosed (s • t)

If G acts on X properly, the set s • t is closed when s : Set G is closed and t : Set X is compact. See also IsClosed.smul_left_of_isCompact for a version with the assumptions on s and t reversed.

Defined in

Mathlib.Topology.Algebra.ProperAction.Basic

Cited by

0 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupMulActionTopologicalSpaceTopologicalSpaceProperSMul