Commit 2023-03-04 10:29 4b79ca50

View on Github →

feat: port Topology.MetricSpace.MetricSeparated (#2608)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/MetricSeparated.lean

added theorem IsMetricSeparated.comm

added theorem IsMetricSeparated.empty_left

added theorem IsMetricSeparated.empty_right

added theorem IsMetricSeparated.finite_unionᵢ_left_iff

added theorem IsMetricSeparated.finite_unionᵢ_right_iff

added theorem IsMetricSeparated.finset_unionᵢ_left_iff

added theorem IsMetricSeparated.finset_unionᵢ_right_iff

added theorem IsMetricSeparated.mono

added theorem IsMetricSeparated.mono_left

added theorem IsMetricSeparated.mono_right

added theorem IsMetricSeparated.subset_compl_right

added theorem IsMetricSeparated.symm

added theorem IsMetricSeparated.union_left

added theorem IsMetricSeparated.union_left_iff

added theorem IsMetricSeparated.union_right

added theorem IsMetricSeparated.union_right_iff

added def IsMetricSeparated