Metric separated pairs of sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define the predicate is_metric_separated. We say that two sets in an (extended)
metric space are metric separated if the (extended) distance between x ∈ s and y ∈ t is
bounded from below by a positive constant.
This notion is useful, e.g., to define metric outer measures.
Two sets in an (extended) metric space are called metric separated if the (extended) distance
between x ∈ s and y ∈ t is bounded from below by a positive constant.
@[symm]
theorem
is_metric_separated.symm
{X : Type u_1}
[emetric_space X]
{s t : set X}
(h : is_metric_separated s t) :
theorem
is_metric_separated.comm
{X : Type u_1}
[emetric_space X]
{s t : set X} :
is_metric_separated s t ↔ is_metric_separated t s
@[simp]
@[simp]
@[protected]
theorem
is_metric_separated.disjoint
{X : Type u_1}
[emetric_space X]
{s t : set X}
(h : is_metric_separated s t) :
disjoint s t
theorem
is_metric_separated.subset_compl_right
{X : Type u_1}
[emetric_space X]
{s t : set X}
(h : is_metric_separated s t) :
theorem
is_metric_separated.mono
{X : Type u_1}
[emetric_space X]
{s t s' t' : set X}
(hs : s ⊆ s')
(ht : t ⊆ t') :
is_metric_separated s' t' → is_metric_separated s t
theorem
is_metric_separated.mono_left
{X : Type u_1}
[emetric_space X]
{s t s' : set X}
(h' : is_metric_separated s' t)
(hs : s ⊆ s') :
theorem
is_metric_separated.mono_right
{X : Type u_1}
[emetric_space X]
{s t t' : set X}
(h' : is_metric_separated s t')
(ht : t ⊆ t') :
theorem
is_metric_separated.union_left
{X : Type u_1}
[emetric_space X]
{s t s' : set X}
(h : is_metric_separated s t)
(h' : is_metric_separated s' t) :
is_metric_separated (s ∪ s') t
@[simp]
theorem
is_metric_separated.union_left_iff
{X : Type u_1}
[emetric_space X]
{s t s' : set X} :
is_metric_separated (s ∪ s') t ↔ is_metric_separated s t ∧ is_metric_separated s' t
theorem
is_metric_separated.union_right
{X : Type u_1}
[emetric_space X]
{s t t' : set X}
(h : is_metric_separated s t)
(h' : is_metric_separated s t') :
is_metric_separated s (t ∪ t')
@[simp]
theorem
is_metric_separated.union_right_iff
{X : Type u_1}
[emetric_space X]
{s t t' : set X} :
is_metric_separated s (t ∪ t') ↔ is_metric_separated s t ∧ is_metric_separated s t'
theorem
is_metric_separated.finite_Union_left_iff
{X : Type u_1}
[emetric_space X]
{ι : Type u_2}
{I : set ι}
(hI : I.finite)
{s : ι → set X}
{t : set X} :
is_metric_separated (⋃ (i : ι) (H : i ∈ I), s i) t ↔ ∀ (i : ι), i ∈ I → is_metric_separated (s i) t
theorem
is_metric_separated.finite_Union_left
{X : Type u_1}
[emetric_space X]
{ι : Type u_2}
{I : set ι}
(hI : I.finite)
{s : ι → set X}
{t : set X} :
(∀ (i : ι), i ∈ I → is_metric_separated (s i) t) → is_metric_separated (⋃ (i : ι) (H : i ∈ I), s i) t
Alias of the reverse direction of is_metric_separated.finite_Union_left_iff.
theorem
is_metric_separated.finite_Union_right_iff
{X : Type u_1}
[emetric_space X]
{ι : Type u_2}
{I : set ι}
(hI : I.finite)
{s : set X}
{t : ι → set X} :
is_metric_separated s (⋃ (i : ι) (H : i ∈ I), t i) ↔ ∀ (i : ι), i ∈ I → is_metric_separated s (t i)
@[simp]
theorem
is_metric_separated.finset_Union_left_iff
{X : Type u_1}
[emetric_space X]
{ι : Type u_2}
{I : finset ι}
{s : ι → set X}
{t : set X} :
is_metric_separated (⋃ (i : ι) (H : i ∈ I), s i) t ↔ ∀ (i : ι), i ∈ I → is_metric_separated (s i) t
theorem
is_metric_separated.finset_Union_left
{X : Type u_1}
[emetric_space X]
{ι : Type u_2}
{I : finset ι}
{s : ι → set X}
{t : set X} :
(∀ (i : ι), i ∈ I → is_metric_separated (s i) t) → is_metric_separated (⋃ (i : ι) (H : i ∈ I), s i) t
Alias of the reverse direction of is_metric_separated.finset_Union_left_iff.
@[simp]
theorem
is_metric_separated.finset_Union_right_iff
{X : Type u_1}
[emetric_space X]
{ι : Type u_2}
{I : finset ι}
{s : set X}
{t : ι → set X} :
is_metric_separated s (⋃ (i : ι) (H : i ∈ I), t i) ↔ ∀ (i : ι), i ∈ I → is_metric_separated s (t i)
theorem
is_metric_separated.finset_Union_right
{X : Type u_1}
[emetric_space X]
{ι : Type u_2}
{I : finset ι}
{s : set X}
{t : ι → set X} :
(∀ (i : ι), i ∈ I → is_metric_separated s (t i)) → is_metric_separated s (⋃ (i : ι) (H : i ∈ I), t i)
Alias of the reverse direction of is_metric_separated.finset_Union_right_iff.