∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s t : Set E}, Absorbs 𝕜 s t → ∀ᶠ (c : 𝕜) in nhdsWithin 0 {0}ᶜ, Set.MapsTo (fun x => c • x) t s