to_properlyDiscontinuousSMul — Mathlib

English

A finite group action is properly discontinuous.

Русский

Действие конечной группы является корректно дискретным.

LaTeX

$$$ProperlyDiscontinuousSMul \Gamma T$$$

Lean4

/-- A finite group action is always properly discontinuous. -/
@[to_additive /-- A finite group action is always properly discontinuous. -/
    ]
instance (priority := 100) to_properlyDiscontinuousSMul [Finite Γ] : ProperlyDiscontinuousSMul Γ T where
  finite_disjoint_inter_image _ _ := Set.toFinite _

Похожие утверждения