English
Absorbent G0 s is equivalent to s containing c^{-1} x eventually for all x under cobounded action.
Русский
Поглощающее множество G0 s эквивалентно тому, что для любого x существует событие, где c^{-1} x ∈ s.
LaTeX
$$$Absorbent G_0 s \\iff \\forall x, \\forall^\\infty c \\in cobounded G_0,\; c^{-1} \\cdot x \\in s$$$
Lean4
theorem absorbent_iff_inv_smul {s : Set α} : Absorbent G₀ s ↔ ∀ x, ∀ᶠ c in cobounded G₀, c⁻¹ • x ∈ s :=
forall_congr' fun x ↦ by simp only [absorbs_iff_eventually_cobounded_mapsTo, mapsTo_singleton]