Local convexity #
This file defines absorbent and balanced sets.
An absorbent set is one that "surrounds" the origin. The idea is made precise by requiring that any point belongs to all large enough scalings of the set. This is the vector world analog of a topological neighborhood of the origin.
A balanced set is one that is everywhere around the origin. This means that a • s ⊆ s
for all a
of norm less than 1
.
Main declarations #
For a module over a normed ring:
Absorbs
: A sets
absorbs a sett
if all large scalings ofs
containt
.Absorbent
: A sets
is absorbent if every point eventually belongs to all large scalings ofs
.Balanced
: A sets
is balanced ifa • s ⊆ s
for alla
of norm less than1
.
References #
Tags #
absorbent, balanced, locally convex, LCTVS
Alias of the forward direction of balanced_iff_smul_mem
.
Alias of the forward direction of absorbs_iff_eventually_nhdsWithin_zero
.
Alias of the forward direction of absorbent_iff_eventually_nhdsWithin_zero
.
Scalar multiplication (by possibly different types) of a balanced set is monotone.
A balanced set absorbs itself.
Alias of Balanced.smul_mem_iff
.
Every neighbourhood of the origin is absorbent.
The union of {0}
with the interior of a balanced set is balanced.
The interior of a balanced set is balanced if it contains the origin.
Alias of Balanced.convexHull
.