absorbent_iff_inv_smul — Mathlib

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]

Похожие утверждения