# Metric separated pairs of sets #

In this file we define the predicate IsMetricSeparated. 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 IsMetricSeparated {X : Type u_1} [] (s : Set X) (t : Set X) :

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
Instances For
theorem IsMetricSeparated.symm {X : Type u_1} [] {s : Set X} {t : Set X} (h : ) :
theorem IsMetricSeparated.comm {X : Type u_1} [] {s : Set X} {t : Set X} :
@[simp]
theorem IsMetricSeparated.empty_left {X : Type u_1} [] (s : Set X) :
@[simp]
theorem IsMetricSeparated.empty_right {X : Type u_1} [] (s : Set X) :
theorem IsMetricSeparated.disjoint {X : Type u_1} [] {s : Set X} {t : Set X} (h : ) :
theorem IsMetricSeparated.subset_compl_right {X : Type u_1} [] {s : Set X} {t : Set X} (h : ) :
s t
theorem IsMetricSeparated.mono {X : Type u_1} [] {s : Set X} {t : Set X} {s' : Set X} {t' : Set X} (hs : s s') (ht : t t') :
theorem IsMetricSeparated.mono_left {X : Type u_1} [] {s : Set X} {t : Set X} {s' : Set X} (h' : ) (hs : s s') :
theorem IsMetricSeparated.mono_right {X : Type u_1} [] {s : Set X} {t : Set X} {t' : Set X} (h' : ) (ht : t t') :
theorem IsMetricSeparated.union_left {X : Type u_1} [] {s : Set X} {t : Set X} {s' : Set X} (h : ) (h' : ) :
@[simp]
theorem IsMetricSeparated.union_left_iff {X : Type u_1} [] {s : Set X} {t : Set X} {s' : Set X} :
theorem IsMetricSeparated.union_right {X : Type u_1} [] {s : Set X} {t : Set X} {t' : Set X} (h : ) (h' : ) :
@[simp]
theorem IsMetricSeparated.union_right_iff {X : Type u_1} [] {s : Set X} {t : Set X} {t' : Set X} :
theorem IsMetricSeparated.finite_iUnion_left_iff {X : Type u_1} [] {ι : Type u_2} {I : Set ι} (hI : I.Finite) {s : ιSet X} {t : Set X} :
IsMetricSeparated (iI, s i) t iI, IsMetricSeparated (s i) t
theorem IsMetricSeparated.finite_iUnion_left {X : Type u_1} [] {ι : Type u_2} {I : Set ι} (hI : I.Finite) {s : ιSet X} {t : Set X} :
(iI, IsMetricSeparated (s i) t)IsMetricSeparated (iI, s i) t

Alias of the reverse direction of IsMetricSeparated.finite_iUnion_left_iff.

theorem IsMetricSeparated.finite_iUnion_right_iff {X : Type u_1} [] {ι : Type u_2} {I : Set ι} (hI : I.Finite) {s : Set X} {t : ιSet X} :
IsMetricSeparated s (iI, t i) iI, IsMetricSeparated s (t i)
@[simp]
theorem IsMetricSeparated.finset_iUnion_left_iff {X : Type u_1} [] {ι : Type u_2} {I : } {s : ιSet X} {t : Set X} :
IsMetricSeparated (iI, s i) t iI, IsMetricSeparated (s i) t
theorem IsMetricSeparated.finset_iUnion_left {X : Type u_1} [] {ι : Type u_2} {I : } {s : ιSet X} {t : Set X} :
(iI, IsMetricSeparated (s i) t)IsMetricSeparated (iI, s i) t

Alias of the reverse direction of IsMetricSeparated.finset_iUnion_left_iff.

@[simp]
theorem IsMetricSeparated.finset_iUnion_right_iff {X : Type u_1} [] {ι : Type u_2} {I : } {s : Set X} {t : ιSet X} :
IsMetricSeparated s (iI, t i) iI, IsMetricSeparated s (t i)
theorem IsMetricSeparated.finset_iUnion_right {X : Type u_1} [] {ι : Type u_2} {I : } {s : Set X} {t : ιSet X} :
(iI, IsMetricSeparated s (t i))IsMetricSeparated s (iI, t i)

Alias of the reverse direction of IsMetricSeparated.finset_iUnion_right_iff.