Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-15 12:40 b5f38321

View on Github →

feat(topology/metric_space): introduce is_metric_separated (#6685)

Estimated changes

Created src/topology/metric_space/metric_separated.lean

added theorem is_metric_separated.comm

added theorem is_metric_separated.empty_left

added theorem is_metric_separated.empty_right

added theorem is_metric_separated.finite_Union_left_iff

added theorem is_metric_separated.finite_Union_right_iff

added theorem is_metric_separated.finset_Union_left_iff

added theorem is_metric_separated.finset_Union_right_iff

added theorem is_metric_separated.mono

added theorem is_metric_separated.mono_left

added theorem is_metric_separated.mono_right

added theorem is_metric_separated.subset_compl_right

added theorem is_metric_separated.symm

added theorem is_metric_separated.union_left

added theorem is_metric_separated.union_left_iff

added theorem is_metric_separated.union_right

added theorem is_metric_separated.union_right_iff

added def is_metric_separated