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