English
In a topological monoid, right multiplication by a right-invertible element preserves cocompactness: if a*b = 1, then x ↦ x*a sends cocompact sets to cocompact sets.
Русский
В топологическом моноиде правое умножение на правый обратимый элемент сохраняет кокомпактность: если a·b = 1, то x ↦ x·a отображает коккомпактные множества в коккомпактные.
LaTeX
$$$\\forall a,b\\,(a\\cdot b = 1)\\; \\text{Tendsto}(\\lambda x, x\\cdot a) (\\text{cocompact } M) (\\text{cocompact } M)$$$
Lean4
/-- Right-multiplication by a right-invertible element of a topological monoid is proper, i.e.,
inverse images of compact sets are compact. -/
theorem tendsto_cocompact_mul_right {a b : M} (ha : a * b = 1) :
Filter.Tendsto (fun x : M => x * a) (Filter.cocompact M) (Filter.cocompact M) :=
by
refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_mul_right b))
simp only [comp_mul_right, ha, mul_one]
exact Filter.tendsto_id
