Theorems · Theorem · Lie groups

IsClosed.smul_left_of_isCompact

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Group α]
  [inst_3 : MulAction α β] [ContinuousInv α] [ContinuousSMul α β] {s : Set α} {t : Set β},
  IsClosed t → IsCompact s → IsClosed (s • t)

If G acts on X continuously, the set s • t is closed when s : Set G is compact and t : Set X is closed. See also IsClosed.smul_right_of_isCompact for a version with the assumptions on s and t reversed, assuming that the action is proper.

Defined in

Mathlib.Topology.Algebra.Group.Pointwise

Cited by

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceGroupMulActionContinuousInvContinuousSMul