Families at bounded distance from a point #
A family at distance at most R ≠ ⊤ from a point has range of finite diameter.
Main results #
TauCeti.ediam_range_ne_top_of_edist_le: the range of such a family has finite diameter.
theorem
TauCeti.ediam_range_ne_top_of_edist_le
{X : Type u_1}
[PseudoEMetricSpace X]
{x : X}
{ι : Type u_2}
{R : ENNReal}
(hR : R ≠ ⊤)
{w : ι → X}
(hw : ∀ (i : ι), edist x (w i) ≤ R)
:
A family at distance at most R ≠ ⊤ from a point has range of finite diameter.