Theorems · Definition · general topology

Absorbs

(M : Type u_1) → {α : Type u_2} → [Bornology M] → [SMul M α] → Set α → Set α → Prop

A set s absorbs another set t if t is contained in all scalings of s by all but a bounded set of elements.

Defined in

Mathlib.Topology.Bornology.Absorbs

Cited by

59 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

BornologySMul