Commit 2025-01-10 22:52 97504000

View on Github →

feat: three lemmas related to Hausdorff distance (#20585) From sphere-eversion, I'm just submitting these.

Estimated changes

Modified Mathlib/Topology/ContinuousOn.lean

added theorem Continuous.tendsto_nhdsSet

added theorem Continuous.tendsto_nhdsSet_nhds

added theorem ContinuousOn.tendsto_nhdsSet

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

added theorem Metric.infDist_pos_iff_not_mem_closure

Modified Mathlib/Topology/MetricSpace/Thickening.lean

added theorem IsCompact.exists_thickening_image_subset

added theorem Metric.thickening_ball

Modified Mathlib/Topology/NhdsSet.lean

deleted theorem Continuous.tendsto_nhdsSet

deleted theorem Continuous.tendsto_nhdsSet_nhds