Thickenings in pseudo-metric spaces #
Main definitions #
Metric.thickening δ s
, the open thickening by radiusδ
of a sets
in a pseudo emetric space.Metric.cthickening δ s
, the closed thickening by radiusδ
of a sets
in a pseudo emetric space.
Main results #
Disjoint.exists_thickenings
: two disjoint sets admit disjoint thickeningsDisjoint.exists_cthickenings
: two disjoint sets admit disjoint closed thickeningsIsCompact.exists_cthickening_subset_open
: ifs
is compact,t
is open ands ⊆ t
, somecthickening
ofs
is contained int
.Metric.hasBasis_nhdsSet_cthickening
: thecthickening
s of a compact setK
form a basis of the neighbourhoods ofK
Metric.closure_eq_iInter_cthickening'
: the closure of a set equals the intersection of its closed thickenings of positive radii accumulating at zero. The same holds for open thickenings.IsCompact.cthickening_eq_biUnion_closedBall
: ifs
is compact,cthickening δ s
is the union ofclosedBall
s of radiusδ
aroundx : E
.
The (open) δ
-thickening Metric.thickening δ E
of a subset E
in a pseudo emetric space
consists of those points that are at distance less than δ
from some point of E
.
Equations
- Metric.thickening δ E = {x : α | EMetric.infEdist x E < ENNReal.ofReal δ}
Instances For
An exterior point of a subset E
(i.e., a point outside the closure of E
) is not in the
(open) δ
-thickening of E
for small enough positive δ
.
The (open) thickening equals the preimage of an open interval under EMetric.infEdist
.
The (open) thickening is an open set.
The (open) thickening of the empty set is empty.
The (open) thickening Metric.thickening δ E
of a fixed subset E
is an increasing function of
the thickening radius δ
.
The (open) thickening Metric.thickening δ E
with a fixed thickening radius δ
is
an increasing function of the subset E
.
The frontier of the (open) thickening of a set is contained in an EMetric.infEdist
level
set.
Any set is contained in the complement of the δ-thickening of the complement of its δ-thickening.
The δ-thickening of the complement of the δ-thickening of a set is contained in the complement of the set.
A point in a metric space belongs to the (open) δ
-thickening of a subset E
if and only if
it is at distance less than δ
from some point of E
.
The (open) δ
-thickening Metric.thickening δ E
of a subset E
in a metric space equals the
union of balls of radius δ
centered at points of E
.
The closed δ
-thickening Metric.cthickening δ E
of a subset E
in a pseudo emetric space
consists of those points that are at infimum distance at most δ
from E
.
Equations
- Metric.cthickening δ E = {x : α | EMetric.infEdist x E ≤ ENNReal.ofReal δ}
Instances For
An exterior point of a subset E
(i.e., a point outside the closure of E
) is not in the
closed δ
-thickening of E
for small enough positive δ
.
The closed thickening is a closed set.
The closed thickening of the empty set is empty.
The closed thickening with radius zero is the closure of the set.
The closed thickening Metric.cthickening δ E
of a fixed subset E
is an increasing function
of the thickening radius δ
.
The closed thickening Metric.cthickening δ E
with a fixed thickening radius δ
is
an increasing function of the subset E
.
The closed thickening Metric.cthickening δ₁ E
is contained in the open thickening
Metric.thickening δ₂ E
if the radius of the latter is positive and larger.
The open thickening Metric.thickening δ E
is contained in the closed thickening
Metric.cthickening δ E
with the same radius.
The closed thickening of a set contains the closure of the set.
The (open) thickening of a set contains the closure of the set.
A set is contained in its own (open) thickening.
A set is contained in its own closed thickening.
If s
is compact, t
is open and s ⊆ t
, some cthickening
of s
is contained in t
.
The closure of a set equals the intersection of its closed thickenings of positive radii accumulating at zero.
The closure of a set equals the intersection of its closed thickenings of positive radii.
The closure of a set equals the intersection of its open thickenings of positive radii accumulating at zero.
The closure of a set equals the intersection of its (open) thickenings of positive radii.
The frontier of the closed thickening of a set is contained in an EMetric.infEdist
level
set.
The closed ball of radius δ
centered at a point of E
is included in the closed
thickening of E
.
The closed thickening of a compact set E
is the union of the balls Metric.closedBall x δ
over x ∈ E
.
See also Metric.cthickening_eq_biUnion_closedBall
.
For the equality, see infEdist_cthickening
.
For the equality, see infEdist_thickening
.
For the equality, see thickening_thickening
.
For the equality, see thickening_cthickening
.
For the equality, see cthickening_thickening
.
For the equality, see cthickening_cthickening
.