Commit 2025-02-15 15:22 6edd1ddf

View on Github →

chore: rename IsMetricSeparated to Metric.AreSeparated (#20911) I need the predicate of a single set to be metric-separated, but the current one which is about two sets is stealing the name. From my PhD (LeanCamCombi)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

Modified Mathlib/Topology/MetricSpace/MetricSeparated.lean

deleted theorem IsMetricSeparated.comm

deleted theorem IsMetricSeparated.empty_left

deleted theorem IsMetricSeparated.empty_right

deleted theorem IsMetricSeparated.finite_iUnion_left_iff

deleted theorem IsMetricSeparated.finite_iUnion_right_iff

deleted theorem IsMetricSeparated.finset_iUnion_left_iff

deleted theorem IsMetricSeparated.finset_iUnion_right_iff

deleted theorem IsMetricSeparated.mono

deleted theorem IsMetricSeparated.mono_left

deleted theorem IsMetricSeparated.mono_right

deleted theorem IsMetricSeparated.subset_compl_right

deleted theorem IsMetricSeparated.symm

deleted theorem IsMetricSeparated.union_left

deleted theorem IsMetricSeparated.union_left_iff

deleted theorem IsMetricSeparated.union_right

deleted theorem IsMetricSeparated.union_right_iff

deleted def IsMetricSeparated

added theorem Metric.AreSeparated.comm

added theorem Metric.AreSeparated.empty_left

added theorem Metric.AreSeparated.empty_right

added theorem Metric.AreSeparated.finite_iUnion_left_iff

added theorem Metric.AreSeparated.finite_iUnion_right_iff

added theorem Metric.AreSeparated.finset_iUnion_left_iff

added theorem Metric.AreSeparated.finset_iUnion_right_iff

added theorem Metric.AreSeparated.mono

added theorem Metric.AreSeparated.mono_left

added theorem Metric.AreSeparated.mono_right

added theorem Metric.AreSeparated.subset_compl_right

added theorem Metric.AreSeparated.symm

added theorem Metric.AreSeparated.union_left

added theorem Metric.AreSeparated.union_left_iff

added theorem Metric.AreSeparated.union_right

added theorem Metric.AreSeparated.union_right_iff

added def Metric.AreSeparated