emetric.inf_edist

The minimal edistance of a point to a set

emetric.inf_edist_union

The edist to a union is the minimum of the edists

emetric.inf_edist_singleton

The edist to a singleton is the edistance to the single point of this singleton

emetric.inf_edist_le_edist_of_mem

The edist to a set is bounded above by the edist to any of its points

emetric.inf_edist_zero_of_mem

If a point x belongs to s, then its edist to s vanishes

emetric.inf_edist_le_inf_edist_of_subset

The edist is monotonous with respect to inclusion

emetric.exists_edist_lt_of_inf_edist_lt

If the edist to a set is < r, there exists a point in the set at edistance < r

emetric.inf_edist_le_inf_edist_add_edist

The edist of x to s is bounded by the sum of the edist of y to s and the edist from x to y

emetric.continuous_inf_edist

The edist to a set depends continuously on the point

emetric.inf_edist_closure

The edist to a set and to its closure coincide

emetric.mem_closure_iff_inf_edist_zero

A point belongs to the closure of s iff its infimum edistance to this set vanishes

emetric.mem_iff_ind_edist_zero_of_closed

Given a closed set s, a point belongs to s iff its infimum edistance to this set vanishes

emetric.inf_edist_image

The infimum edistance is invariant under isometries

emetric.Hausdorff_edist

The Hausdorff edistance between two sets is the smallest r such that each set is contained in the r-neighborhood of the other one

emetric.Hausdorff_edist_self

The Hausdorff edistance of a set to itself vanishes

emetric.Hausdorff_edist_comm

The Haudorff edistances of s to t and of t to s coincide

emetric.Hausdorff_edist_le_of_inf_edist

Bounding the Hausdorff edistance by bounding the edistance of any point in each set to the other set

emetric.Hausdorff_edist_le_of_mem_edist

Bounding the Hausdorff edistance by exhibiting, for any point in each set, another point in the other set at controlled distance

emetric.inf_edist_le_Hausdorff_edist_of_mem

The distance to a set is controlled by the Hausdorff distance

emetric.exists_edist_lt_of_Hausdorff_edist_lt

If the Hausdorff distance is <r, then any point in one of the sets has a corresponding point at distance <r in the other set

emetric.inf_edist_le_inf_edist_add_Hausdorff_edist

The distance from x to sor t is controlled in terms of the Hausdorff distance between s and t

emetric.Hausdorff_edist_image

The Hausdorff edistance is invariant under eisometries

emetric.Hausdorff_edist_le_ediam

The Hausdorff distance is controlled by the diameter of the union

emetric.Hausdorff_edist_triangle

The Hausdorff distance satisfies the triangular inequality

emetric.Hausdorff_edist_self_closure

The Hausdorff edistance between a set and its closure vanishes

emetric.Hausdorff_edist_closure₁

Replacing a set by its closure does not change the Hausdorff edistance.

emetric.Hausdorff_edist_closure₂

Replacing a set by its closure does not change the Hausdorff edistance.

emetric.Hausdorff_edist_closure

The Hausdorff edistance between sets or their closures is the same

emetric.Hausdorff_edist_zero_iff_closure_eq_closure

Two sets are at zero Hausdorff edistance if and only if they have the same closure

emetric.Hausdorff_edist_zero_iff_eq_of_closed

Two closed sets are at zero Hausdorff edistance if and only if they coincide

emetric.Hausdorff_edist_empty

The Haudorff edistance to the empty set is infinite

emetric.ne_empty_of_Hausdorff_edist_ne_top

If a set is at finite Hausdorff edistance of a nonempty set, it is nonempty

metric.inf_dist

The minimal distance of a point to a set

metric.inf_dist_nonneg

the minimal distance is always nonnegative

metric.inf_dist_empty

the minimal distance to the empty set is 0 (if you want to have the more reasonable value ∞ instead, use inf_edist, which takes values in ennreal)

metric.inf_edist_ne_top

In a metric space, the minimal edistance to a nonempty set is finite

metric.inf_dist_zero_of_mem

The minimal distance of a point to a set containing it vanishes

metric.inf_dist_singleton

The minimal distance to a singleton is the distance to the unique point in this singleton

metric.inf_dist_le_dist_of_mem

The minimal distance to a set is bounded by the distance to any point in this set

metric.inf_dist_le_inf_dist_of_subset

The minimal distance is monotonous with respect to inclusion

metric.exists_dist_lt_of_inf_dist_lt

If the minimal distance to a set is <r, there exists a point in this set at distance <r

metric.inf_dist_le_inf_dist_add_dist

The minimal distance from x to s is bounded by the distance from y to s, modulo the distance between x and y

metric.uniform_continuous_inf_dist

The minimal distance to a set is uniformly continuous

metric.continuous_inf_dist

The minimal distance to a set is continuous

metric.inf_dist_eq_closure

The minimal distance to a set and its closure coincide

metric.mem_closure_iff_inf_dist_zero

A point belongs to the closure of s iff its infimum distance to this set vanishes

metric.mem_iff_inf_dist_zero_of_closed

Given a closed set s, a point belongs to s iff its infimum distance to this set vanishes

metric.inf_dist_image

The infimum distance is invariant under isometries

metric.Hausdorff_dist

The Hausdorff distance between two sets is the smallest nonnegative r such that each set is included in the r-neighborhood of the other. If there is no such r, it is defined to be 0, arbitrarily

metric.Hausdorff_dist_nonneg

The Hausdorff distance is nonnegative

metric.Hausdorff_edist_ne_top_of_ne_empty_of_bounded

If two sets are nonempty and bounded in a metric space, they are at finite Hausdorff edistance

metric.Hausdorff_dist_self_zero

The Hausdorff distance between a set and itself is zero

metric.Hausdorff_dist_comm

The Hausdorff distance from s to t and from t to s coincide

metric.Hausdorff_dist_empty

The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable value ∞ instead, use Hausdorff_edist, which takes values in ennreal)

metric.Hausdorff_dist_empty'

The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable value ∞ instead, use Hausdorff_edist, which takes values in ennreal)

metric.Hausdorff_dist_le_of_inf_dist

Bounding the Hausdorff distance by bounding the distance of any point in each set to the other set

metric.Hausdorff_dist_le_of_mem_dist

Bounding the Hausdorff distance by exhibiting, for any point in each set, another point in the other set at controlled distance

metric.Hausdorff_dist_le_diam

The Hausdorff distance is controlled by the diameter of the union

metric.inf_dist_le_Hausdorff_dist_of_mem

The distance to a set is controlled by the Hausdorff distance

metric.exists_dist_lt_of_Hausdorff_dist_lt

If the Hausdorff distance is <r, then any point in one of the sets is at distance <r of a point in the other set

metric.exists_dist_lt_of_Hausdorff_dist_lt'

If the Hausdorff distance is <r, then any point in one of the sets is at distance <r of a point in the other set

metric.inf_dist_le_inf_dist_add_Hausdorff_dist

The infimum distance to s and t are the same, up to the Hausdorff distance between s and t

metric.Hausdorff_dist_image

The Hausdorff distance is invariant under isometries

metric.Hausdorff_dist_triangle

The Hausdorff distance satisfies the triangular inequality

metric.Hausdorff_dist_triangle'

The Hausdorff distance satisfies the triangular inequality

metric.Hausdorff_dist_self_closure

The Hausdorff distance between a set and its closure vanish

metric.Hausdorff_dist_closure₁

Replacing a set by its closure does not change the Hausdorff distance.

metric.Hausdorff_dist_closure₂

Replacing a set by its closure does not change the Hausdorff distance.

metric.Hausdorff_dist_closure

The Hausdorff distance between two sets and their closures coincide

metric.Hausdorff_dist_zero_iff_closure_eq_closure

Two sets are at zero Hausdorff distance if and only if they have the same closures

metric.Hausdorff_dist_zero_iff_eq_of_closed

Two closed sets are at zero Hausdorff distance if and only if they coincide