English
If S acts properly discontinuously on G, then the opposite subgroup S.op acting on G by right multiplication is properly discontinuous as well.
Русский
Если S действует правильно прерывающе на G, то противоположная подгруппа S.op действует справа также правильно прерывающе.
LaTeX
$$$\text{ProperlyDiscontinuousSMul}(S^{\mathrm{op}}, G)$ under the opposite action.$$
Lean4
/-- A subgroup `S` of a topological group `G` acts on `G` properly discontinuously on the right, if
it is discrete in the sense that `S ∩ K` is finite for all compact `K`. (See also
`DiscreteTopology`.)
If `G` is Hausdorff, this can be combined with `t2Space_of_properlyDiscontinuousSMul_of_t2Space`
to show that the quotient group `G ⧸ S` is Hausdorff. -/
@[to_additive /-- A subgroup `S` of an additive topological group `G` acts on `G` properly discontinuously
on the right, if it is discrete in the sense that `S ∩ K` is finite for all compact `K`.
(See also `DiscreteTopology`.)
If `G` is Hausdorff, this can be combined with `t2Space_of_properlyDiscontinuousVAdd_of_t2Space`
to show that the quotient group `G ⧸ S` is Hausdorff. -/
]
theorem properlyDiscontinuousSMul_opposite_of_tendsto_cofinite (S : Subgroup G)
(hS : Tendsto S.subtype cofinite (cocompact G)) : ProperlyDiscontinuousSMul S.op G :=
{
finite_disjoint_inter_image := by
intro K L hK hL
have : Continuous fun p : G × G => (p.1⁻¹, p.2) := continuous_inv.prodMap continuous_id
have H : Set.Finite _ := hS ((hK.prod hL).image (continuous_mul.comp this)).compl_mem_cocompact
simp only [preimage_compl, compl_compl, coe_subtype, comp_apply] at H
apply Finite.of_preimage _ (equivOp S).surjective
convert H using 1
ext x
simp only [image_smul, mem_setOf_eq, mem_preimage, mem_image, Prod.exists]
exact Set.op_smul_inter_ne_empty_iff }
