Properly discontinuous actions of subgroups

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

theorem AddSubgroup.properlyDiscontinuousVAdd_iff {Γ : Type u_1} {α : Type u_2} [AddGroup Γ] [TopologicalSpace α] [VAdd Γ α] (S : AddSubgroup Γ) : ProperlyDiscontinuousVAdd (↥S) α ↔ ∀ {K L : Set α}, IsCompact K → IsCompact L → {g : Γ | g ∈ S ∧ ((g +ᵥ K) ∩ L).Nonempty}.Finite

theorem Subgroup.properlyDiscontinuousSMul_of_le {Γ : Type u_1} {α : Type u_2} [Group Γ] [TopologicalSpace α] [SMul Γ α] {G H : Subgroup Γ} (hG : ProperlyDiscontinuousSMul (↥G) α) (hGH : H ≤ G) : ProperlyDiscontinuousSMul (↥H) α

theorem AddSubgroup.properlyDiscontinuousVAdd_of_le {Γ : Type u_1} {α : Type u_2} [AddGroup Γ] [TopologicalSpace α] [VAdd Γ α] {G H : AddSubgroup Γ} (hG : ProperlyDiscontinuousVAdd (↥G) α) (hGH : H ≤ G) : ProperlyDiscontinuousVAdd (↥H) α

instance instProperlyDiscontinuousSMulSubtypeMemSubgroup {Γ : Type u_1} {α : Type u_2} [Group Γ] [TopologicalSpace α] [SMul Γ α] [ProperlyDiscontinuousSMul Γ α] (G : Subgroup Γ) : ProperlyDiscontinuousSMul (↥G) α

If Γ acts properly discontinuously, so does every subgroup of Γ.

instance instProperlyDiscontinuousVAddSubtypeMemAddSubgroup {Γ : Type u_1} {α : Type u_2} [AddGroup Γ] [TopologicalSpace α] [VAdd Γ α] [ProperlyDiscontinuousVAdd Γ α] (G : AddSubgroup Γ) : ProperlyDiscontinuousVAdd (↥G) α

If Γ acts properly discontinuously, so does every additive subgroup of Γ.

theorem ProperlyDiscontinuousSMul.ofFiniteRelIndex {Γ : Type u_1} {α : Type u_2} [Group Γ] [TopologicalSpace α] [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.

theorem ProperlyDiscontinuousVAdd.ofFiniteRelIndex {Γ : Type u_1} {α : Type u_2} [AddGroup Γ] [TopologicalSpace α] [AddAction Γ α] [ContinuousConstVAdd Γ α] (G H : AddSubgroup Γ) [hH : ProperlyDiscontinuousVAdd (↥H) α] [H.IsFiniteRelIndex G] : ProperlyDiscontinuousVAdd (↥G) α

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

theorem Subgroup.properlyDiscontinuousSMul_iff_of_isFiniteRelIndex {Γ : Type u_1} {α : Type u_2} [Group Γ] [TopologicalSpace α] [MulAction Γ α] [ContinuousConstSMul Γ α] {G H : Subgroup Γ} (hGH : G ≤ H) [G.IsFiniteRelIndex H] : ProperlyDiscontinuousSMul (↥G) α ↔ ProperlyDiscontinuousSMul (↥H) α

theorem AddSubgroup.properlyDiscontinuousVAdd_iff_of_isFiniteRelIndex {Γ : Type u_1} {α : Type u_2} [AddGroup Γ] [TopologicalSpace α] [AddAction Γ α] [ContinuousConstVAdd Γ α] {G H : AddSubgroup Γ} (hGH : G ≤ H) [G.IsFiniteRelIndex H] : ProperlyDiscontinuousVAdd (↥G) α ↔ ProperlyDiscontinuousVAdd (↥H) α

theorem Subgroup.Commensurable.properlyDiscontinuousSMul_iff {Γ : Type u_1} {α : Type u_2} [Group Γ] [TopologicalSpace α] [MulAction Γ α] [ContinuousConstSMul Γ α] {G H : Subgroup Γ} (h : G.Commensurable H) : ProperlyDiscontinuousSMul (↥G) α ↔ ProperlyDiscontinuousSMul (↥H) α

theorem AddSubgroup.Commensurable.properlyDiscontinuousVAdd_iff {Γ : Type u_1} {α : Type u_2} [AddGroup Γ] [TopologicalSpace α] [AddAction Γ α] [ContinuousConstVAdd Γ α] {G H : AddSubgroup Γ} (h : G.Commensurable H) : ProperlyDiscontinuousVAdd (↥G) α ↔ ProperlyDiscontinuousVAdd (↥H) α