absorbs_iff_eventually_cobounded_mapsTo

English

Absorbs G0 s t is equivalent to the eventual coboundedness of maps, i.e., Absorbs G0 s t iff Eventually (MapsTo (c⁻¹•·) t s) in cobounded G0.

Русский

Поглощение s по отношению к t эквивалентно существованию предельного поведения отображения MapsTo при cobounded G0.

LaTeX

$$Iff (Absorbs G_0 s t) (Filter.Eventually (fun c => MapsTo (c^{-1} \cdot) t s) (inst_1.cobounded G_0))$$

Lean4

theorem absorbs_iff_eventually_cobounded_mapsTo : Absorbs G₀ s t ↔ ∀ᶠ c in cobounded G₀, MapsTo (c⁻¹ • ·) t s :=
  eventually_congr <| (eventually_ne_cobounded 0).mono fun c hc ↦ by rw [← preimage_smul_inv₀ hc]; rfl

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