mathlib
ed269dd5 - Move two lemmas to hausdorff_distance.lean.

Commit

3 years ago

Move two lemmas to hausdorff_distance.lean.

References

#17648 - feat(topology/metric_space/thickened_indicator): Add convergence of plain old indicators of thickenings.

Author

kkytola

kkytola

Parents

Loading