English
If a subgroup S of a topological group G is discrete in the sense that S ∩ K is finite for every compact K, then the left action of S on G is properly discontinuous.
Русский
Если подгруппа S топологической группы G дискретна в смысле того, что S ∩ K конечна для каждого компактного K, то левая действия S на G является нормально разъешьенной (правильно прерываемой).
LaTeX
$$$\text{ProperlyDiscontinuousSMul } S G$ if S ∩ K is finite for all compact K (in the appropriate sense).$$
Lean4
/-- A subgroup `S` of a topological group `G` acts on `G` properly discontinuously on the left, if
it is discrete in the sense that `S ∩ K` is finite for all compact `K`. (See also
`DiscreteTopology`.) -/
@[to_additive /-- A subgroup `S` of an additive topological group `G` acts on `G` properly
discontinuously on the left, if it is discrete in the sense that `S ∩ K` is finite for all compact
`K`. (See also `DiscreteTopology`. -/
]
theorem properlyDiscontinuousSMul_of_tendsto_cofinite (S : Subgroup G) (hS : Tendsto S.subtype cofinite (cocompact G)) :
ProperlyDiscontinuousSMul S G :=
{
finite_disjoint_inter_image := by
intro K L hK hL
have H : Set.Finite _ := hS ((hL.prod hK).image continuous_div').compl_mem_cocompact
rw [preimage_compl, compl_compl] at H
convert H
ext x
simp only [image_smul, mem_setOf_eq, coe_subtype, mem_preimage, mem_image, Prod.exists]
exact Set.smul_inter_ne_empty_iff' }
