NRR.Multivalued.Separator.Distance — distance to a closed nonempty set

Thin project wrappers around Metric.infDist packaging the metric facts used by the signed-distance construction: continuity, vanishing on the underlying set, strict positivity outside a closed nonempty set, the membership characterization of zero distance, and the estimate by the distance to any chosen point of the set.

All results are stated for a general metric space; no compactness is assumed. Positivity requires both closedness and nonemptiness of the set.

theorem NRR.MetricTools.continuous_infDist {Z : Type u_1} [MetricSpace Z] (S : Set Z) : Continuous fun (z : Z) => Metric.infDist z S

Distance to a set is a continuous function of the point (Mathlib's 1-Lipschitz theorem).

theorem NRR.MetricTools.infDist_eq_zero_of_mem {Z : Type u_1} [MetricSpace Z] {S : Set Z} {z : Z} (hz : z ∈ S) : Metric.infDist z S = 0

A point of the set has zero distance to the set.

theorem NRR.MetricTools.infDist_pos_of_not_mem {Z : Type u_1} [MetricSpace Z] {S : Set Z} (hSclosed : IsClosed S) (hSne : S.Nonempty) {z : Z} (hz : z ∉ S) : 0 < Metric.infDist z S

Outside a closed nonempty set the distance is strictly positive.

theorem NRR.MetricTools.infDist_eq_zero_iff {Z : Type u_1} [MetricSpace Z] {S : Set Z} (hSclosed : IsClosed S) (hSne : S.Nonempty) {z : Z} : Metric.infDist z S = 0 ↔ z ∈ S

For a closed nonempty set, zero distance characterizes membership.

theorem NRR.MetricTools.infDist_le_dist_of_mem {Z : Type u_1} [MetricSpace Z] {S : Set Z} {z s : Z} (hs : s ∈ S) : Metric.infDist z S ≤ dist z s

The distance to the set is bounded by the distance to any of its points.

theorem NRR.MetricTools.abs_infDist_le_dist_of_mem {Z : Type u_1} [MetricSpace Z] {S : Set Z} {z s : Z} (hs : s ∈ S) : |Metric.infDist z S| ≤ dist z s

The absolute value of the distance is bounded by the distance to any point of the set.