Theorems · Theorem · manifolds

IsClosed.vadd_right_of_isCompact

∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ProperVAdd 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. In particular, this applies when the action comes from an IsTopologicalAddTorsor. See also IsClosed.vadd_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

AddGroupAddActionTopologicalSpaceTopologicalSpaceProperVAdd