mathlibdocumentation

topology.metric_space.metric_separated

Metric separated pairs of sets #

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.

def is_metric_separated {X : Type u_1} (s t : set X) :
Prop

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.

Equations
@[symm]
theorem is_metric_separated.symm {X : Type u_1} {s t : set X} (h : t) :
theorem is_metric_separated.comm {X : Type u_1} {s t : set X} :
@[simp]
theorem is_metric_separated.empty_left {X : Type u_1} (s : set X) :
@[simp]
theorem is_metric_separated.empty_right {X : Type u_1} (s : set X) :
@[protected]
theorem is_metric_separated.disjoint {X : Type u_1} {s t : set X} (h : t) :
t
theorem is_metric_separated.subset_compl_right {X : Type u_1} {s t : set X} (h : t) :
s t
theorem is_metric_separated.mono {X : Type u_1} {s t s' t' : set X} (hs : s s') (ht : t t') :
t'
theorem is_metric_separated.mono_left {X : Type u_1} {s t s' : set X} (h' : t) (hs : s s') :
theorem is_metric_separated.mono_right {X : Type u_1} {s t t' : set X} (h' : t') (ht : t t') :
theorem is_metric_separated.union_left {X : Type u_1} {s t s' : set X} (h : t) (h' : t) :
@[simp]
theorem is_metric_separated.union_left_iff {X : Type u_1} {s t s' : set X} :
theorem is_metric_separated.union_right {X : Type u_1} {s t t' : set X} (h : t) (h' : t') :
(t t')
@[simp]
theorem is_metric_separated.union_right_iff {X : Type u_1} {s t t' : set X} :
(t t')
theorem is_metric_separated.finite_Union_left_iff {X : Type u_1} {ι : 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 Iis_metric_separated (s i) t
theorem is_metric_separated.finite_Union_left {X : Type u_1} {ι : Type u_2} {I : set ι} (hI : I.finite) {s : ι → set X} {t : set X} :
(∀ (i : ι), i Iis_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} {ι : Type u_2} {I : set ι} (hI : I.finite) {s : set X} {t : ι → set X} :
(⋃ (i : ι) (H : i I), t i) ∀ (i : ι), i I (t i)
@[simp]
theorem is_metric_separated.finset_Union_left_iff {X : Type u_1} {ι : Type u_2} {I : finset ι} {s : ι → set X} {t : set X} :
is_metric_separated (⋃ (i : ι) (H : i I), s i) t ∀ (i : ι), i Iis_metric_separated (s i) t
theorem is_metric_separated.finset_Union_left {X : Type u_1} {ι : Type u_2} {I : finset ι} {s : ι → set X} {t : set X} :
(∀ (i : ι), i Iis_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} {ι : Type u_2} {I : finset ι} {s : set X} {t : ι → set X} :
(⋃ (i : ι) (H : i I), t i) ∀ (i : ι), i I (t i)
theorem is_metric_separated.finset_Union_right {X : Type u_1} {ι : Type u_2} {I : finset ι} {s : set X} {t : ι → set X} :
(∀ (i : ι), i I (t i)) (⋃ (i : ι) (H : i I), t i)

Alias of the reverse direction of is_metric_separated.finset_Union_right_iff.