Theorems · Theorem · Lie groups

AddSubgroup.properlyDiscontinuousVAdd_iff

∀ {Γ : Type u_1} {α : Type u_2} [inst : AddGroup Γ] [inst_1 : TopologicalSpace α] [inst_2 : VAdd Γ α]
  (S : AddSubgroup Γ),
  ProperlyDiscontinuousVAdd (↥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: AddGroup TopologicalSpace VAdd

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
Set.ofPredstatement and proof · cited by 6,101
Set.imageproof · cited by 5,609
AddGroupstatement and proof · cited by 4,410
AddSubgroupstatement and proof · cited by 3,232
Set.Nonemptystatement and proof · cited by 2,627
Set.extproof · cited by 2,266
HVAdd.hVAddstatement and proof · cited by 1,820
Set.Finitestatement and proof · cited by 1,814
IsCompactstatement and proof · cited by 1,282
VAddstatement and proof · cited by 616

Cited by2

Results whose statement or proof uses this declaration.

ProperlyDiscontinuousVAdd.ofFiniteRelIndexproof · cited by 1
AddSubgroup.properlyDiscontinuousVAdd_of_leproof · cited by 1