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} [EMetricSpace 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

• IsMetricSeparated s t = ∃ (r : ENNReal), r ≠ 0 ∧ ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y

theorem IsMetricSeparated.symm {X : Type u_1} [EMetricSpace X] {s t : Set X} (h : IsMetricSeparated s t) : IsMetricSeparated t s

theorem IsMetricSeparated.comm {X : Type u_1} [EMetricSpace X] {s t : Set X} : IsMetricSeparated s t ↔ IsMetricSeparated t s

@[simp]

theorem IsMetricSeparated.empty_left {X : Type u_1} [EMetricSpace X] (s : Set X) : IsMetricSeparated ∅ s

@[simp]

theorem IsMetricSeparated.empty_right {X : Type u_1} [EMetricSpace X] (s : Set X) : IsMetricSeparated s ∅

theorem IsMetricSeparated.disjoint {X : Type u_1} [EMetricSpace X] {s t : Set X} (h : IsMetricSeparated s t) : Disjoint s t

theorem IsMetricSeparated.subset_compl_right {X : Type u_1} [EMetricSpace X] {s t : Set X} (h : IsMetricSeparated s t) : s ⊆ tᶜ

theorem IsMetricSeparated.mono {X : Type u_1} [EMetricSpace X] {s t s' t' : Set X} (hs : s ⊆ s') (ht : t ⊆ t') : IsMetricSeparated s' t' → IsMetricSeparated s t

theorem IsMetricSeparated.mono_left {X : Type u_1} [EMetricSpace X] {s t s' : Set X} (h' : IsMetricSeparated s' t) (hs : s ⊆ s') : IsMetricSeparated s t

theorem IsMetricSeparated.mono_right {X : Type u_1} [EMetricSpace X] {s t t' : Set X} (h' : IsMetricSeparated s t') (ht : t ⊆ t') : IsMetricSeparated s t

theorem IsMetricSeparated.union_left {X : Type u_1} [EMetricSpace X] {s t s' : Set X} (h : IsMetricSeparated s t) (h' : IsMetricSeparated s' t) : IsMetricSeparated (s ∪ s') t

@[simp]

theorem IsMetricSeparated.union_left_iff {X : Type u_1} [EMetricSpace X] {s t s' : Set X} : IsMetricSeparated (s ∪ s') t ↔ IsMetricSeparated s t ∧ IsMetricSeparated s' t

theorem IsMetricSeparated.union_right {X : Type u_1} [EMetricSpace X] {s t t' : Set X} (h : IsMetricSeparated s t) (h' : IsMetricSeparated s t') : IsMetricSeparated s (t ∪ t')

@[simp]

theorem IsMetricSeparated.union_right_iff {X : Type u_1} [EMetricSpace X] {s t t' : Set X} : IsMetricSeparated s (t ∪ t') ↔ IsMetricSeparated s t ∧ IsMetricSeparated s t'

theorem IsMetricSeparated.finite_iUnion_left_iff {X : Type u_1} [EMetricSpace X] {ι : Type u_2} {I : Set ι} (hI : I.Finite) {s : ι → Set X} {t : Set X} : IsMetricSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, IsMetricSeparated (s i) t

theorem IsMetricSeparated.finite_iUnion_left {X : Type u_1} [EMetricSpace X] {ι : Type u_2} {I : Set ι} (hI : I.Finite) {s : ι → Set X} {t : Set X} : (∀ i ∈ I, IsMetricSeparated (s i) t) → IsMetricSeparated (⋃ i ∈ I, s i) t

Alias of the reverse direction of IsMetricSeparated.finite_iUnion_left_iff.

theorem IsMetricSeparated.finite_iUnion_right_iff {X : Type u_1} [EMetricSpace X] {ι : Type u_2} {I : Set ι} (hI : I.Finite) {s : Set X} {t : ι → Set X} : IsMetricSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, IsMetricSeparated s (t i)

@[simp]

theorem IsMetricSeparated.finset_iUnion_left_iff {X : Type u_1} [EMetricSpace X] {ι : Type u_2} {I : Finset ι} {s : ι → Set X} {t : Set X} : IsMetricSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, IsMetricSeparated (s i) t

theorem IsMetricSeparated.finset_iUnion_left {X : Type u_1} [EMetricSpace X] {ι : Type u_2} {I : Finset ι} {s : ι → Set X} {t : Set X} : (∀ i ∈ I, IsMetricSeparated (s i) t) → IsMetricSeparated (⋃ i ∈ I, 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} [EMetricSpace X] {ι : Type u_2} {I : Finset ι} {s : Set X} {t : ι → Set X} : IsMetricSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, IsMetricSeparated s (t i)

theorem IsMetricSeparated.finset_iUnion_right {X : Type u_1} [EMetricSpace X] {ι : Type u_2} {I : Finset ι} {s : Set X} {t : ι → Set X} : (∀ i ∈ I, IsMetricSeparated s (t i)) → IsMetricSeparated s (⋃ i ∈ I, t i)

Alias of the reverse direction of IsMetricSeparated.finset_iUnion_right_iff.