Theorems · Theorem · Lie groups

IsClosed.vadd_left_of_isCompact

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup α]
  [inst_3 : AddAction α β] [ContinuousNeg α] [ContinuousVAdd α β] {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.vadd_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

TopologicalSpaceTopologicalSpaceAddGroupAddActionContinuousNegContinuousVAdd