Theorems · Theorem · general topology

eventually_cobounded_mapsTo

∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α]
  {s t : Set α}, Absorbs G₀ s t → ∀ᶠ (c : G₀) in Bornology.cobounded G₀, Set.MapsTo (fun x => c⁻¹ • x) t s

Alias of the forward direction of absorbs_iff_eventually_cobounded_mapsTo.

Defined in

Mathlib.Topology.Bornology.Absorbs

Cited by

0 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupWithZeroBornologyMulAction