Theorems · Theorem · Lie groups

ProperlyDiscontinuousSMul.ofFiniteRelIndex

∀ {Γ : Type u_1} {α : Type u_2} [inst : Group Γ] [inst_1 : TopologicalSpace α] [inst_2 : MulAction Γ α]
  [ContinuousConstSMul Γ α] (G H : Subgroup Γ) [hH : ProperlyDiscontinuousSMul (↥H) α] [H.IsFiniteRelIndex G],
  ProperlyDiscontinuousSMul (↥G) α

If G, H are subgroups of Γ which acts on α, and G ∩ H has finite index in G, then G acts properly discontinuously if H does.

Defined in

Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupTopologicalSpaceMulActionContinuousConstSMulProperlyDiscontinuousSMulSubgroup.IsFiniteRelIndex