Theorems · Theorem · Lie groups

Subgroup.properlyDiscontinuousSMul_iff

∀ {Γ : Type u_1} {α : Type u_2} [inst : Group Γ] [inst_1 : TopologicalSpace α] [inst_2 : SMul Γ α] (S : Subgroup Γ),
  ProperlyDiscontinuousSMul (↥S) α ↔
    ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ S ∧ (g • K ∩ L).Nonempty}.Finite

Defined in

Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupTopologicalSpaceSMul