Hausdorff measure of connected sets

A preconnected set has one-dimensional Hausdorff measure at least its extended diameter.

theorem LeanPool.Besicovitch.edist_le_hausdorffMeasure_one_of_isPreconnected {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} (hs : IsPreconnected s) {x y : X} (hx : x ∈ s) (hy : y ∈ s) : edist x y ≤ (MeasureTheory.Measure.hausdorffMeasure 1) s

The Hausdorff one-measure of a preconnected set bounds the distance between its points.

theorem LeanPool.Besicovitch.ediam_le_hausdorffMeasure_one_of_isPreconnected {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} (hs : IsPreconnected s) : Metric.ediam s ≤ (MeasureTheory.Measure.hausdorffMeasure 1) s

The Hausdorff one-measure of a preconnected set bounds its extended diameter.