mathlib documentation

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} [emetric_space X] (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
theorem is_metric_separated.symm {X : Type u_1} [emetric_space X] {s t : set X} (h : is_metric_separated s t) :
@[simp]
theorem is_metric_separated.empty_left {X : Type u_1} [emetric_space X] (s : set X) :
@[simp]
theorem is_metric_separated.empty_right {X : Type u_1} [emetric_space X] (s : set X) :
theorem is_metric_separated.disjoint {X : Type u_1} [emetric_space X] {s t : set X} (h : is_metric_separated 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) :
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') :
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) :
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') :
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 Iis_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 Iis_metric_separated (s i) t)is_metric_separated (⋃ (i : ι) (H : i I), s i) t

Alias of 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 Iis_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 Iis_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 Iis_metric_separated (s i) t)is_metric_separated (⋃ (i : ι) (H : i I), s i) t

Alias of 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 Iis_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 Iis_metric_separated s (t i))is_metric_separated s (⋃ (i : ι) (H : i I), t i)

Alias of finset_Union_right_iff.