Theorems · Theorem · general topology

absorbs_iff_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

Defined in

Mathlib.Topology.Bornology.Absorbs

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupWithZeroBornologyMulAction