Metric separation

This file defines a few notions of separations of sets in a metric space.

The first notion (Metric.IsSeparated) is quantitative and about a single set: A set s is ε-separated if its elements are pairwise at distance at least ε from each other.

The second notion (Metric.AreSeparated) is qualitative and about two sets: Two sets s and t are separated if the distance between x ∈ s and y ∈ t is bounded from below by a positive constant.

Metric-separated sets

In this section we define the predicate Metric.IsSeparated for ε-separated sets.

def Metric.IsSeparated {X : Type u_1} [PseudoEMetricSpace X] (ε : ENNReal) (s : Set X) : Prop

A set s is ε-separated if its elements are pairwise at distance at least ε from each other.

Equations

• Metric.IsSeparated ε s = s.Pairwise fun (x1 x2 : X) => ε < edist x1 x2

theorem Metric.IsSeparated.empty {X : Type u_1} [PseudoEMetricSpace X] {ε : ENNReal} : IsSeparated ε ∅

theorem Metric.IsSeparated.singleton {X : Type u_1} [PseudoEMetricSpace X] {ε : ENNReal} {x : X} : IsSeparated ε {x}

@[simp]

theorem Metric.IsSeparated.of_subsingleton {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : ENNReal} (hs : s.Subsingleton) : IsSeparated ε s

theorem Set.Subsingleton.isSeparated {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : ENNReal} (hs : s.Subsingleton) : Metric.IsSeparated ε s

Alias of Metric.IsSeparated.of_subsingleton.

theorem Metric.IsSeparated.anti {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε δ : ENNReal} (hεδ : ε ≤ δ) (hs : IsSeparated δ s) : IsSeparated ε s

theorem Metric.IsSeparated.subset {X : Type u_1} [PseudoEMetricSpace X] {s t : Set X} {ε : ENNReal} (hst : s ⊆ t) (hs : IsSeparated ε t) : IsSeparated ε s

theorem Metric.isSeparated_insert {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : ENNReal} {x : X} : IsSeparated ε (insert x s) ↔ IsSeparated ε s ∧ ∀ y ∈ s, x ≠ y → ε < edist x y

theorem Metric.isSeparated_insert_of_notMem {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : ENNReal} {x : X} (hx : x ∉ s) : IsSeparated ε (insert x s) ↔ IsSeparated ε s ∧ ∀ y ∈ s, ε < edist x y

@[deprecated Metric.isSeparated_insert_of_notMem (since := "2025-05-23")]

theorem Metric.isSeparated_insert_of_not_mem {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : ENNReal} {x : X} (hx : x ∉ s) : IsSeparated ε (insert x s) ↔ IsSeparated ε s ∧ ∀ y ∈ s, ε < edist x y

Alias of Metric.isSeparated_insert_of_notMem.

theorem Metric.IsSeparated.insert {X : Type u_1} [PseudoEMetricSpace X] {s : Set X} {ε : ENNReal} {x : X} (hs : IsSeparated ε s) (h : ∀ y ∈ s, x ≠ y → ε < edist x y) : IsSeparated ε (insert x s)

Metric separated pairs of sets

In this section we define the predicate Metric.AreSeparated. 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 Metric.AreSeparated {X : Type u_1} [PseudoEMetricSpace 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

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

theorem Metric.AreSeparated.symm {X : Type u_1} [PseudoEMetricSpace X] {s t : Set X} (h : AreSeparated s t) : AreSeparated t s

theorem Metric.AreSeparated.comm {X : Type u_1} [PseudoEMetricSpace X] {s t : Set X} : AreSeparated s t ↔ AreSeparated t s

@[simp]

theorem Metric.AreSeparated.empty_left {X : Type u_1} [PseudoEMetricSpace X] (s : Set X) : AreSeparated ∅ s

@[simp]

theorem Metric.AreSeparated.empty_right {X : Type u_1} [PseudoEMetricSpace X] (s : Set X) : AreSeparated s ∅

theorem Metric.AreSeparated.disjoint {X : Type u_1} [PseudoEMetricSpace X] {s t : Set X} (h : AreSeparated s t) : Disjoint s t

theorem Metric.AreSeparated.subset_compl_right {X : Type u_1} [PseudoEMetricSpace X] {s t : Set X} (h : AreSeparated s t) : s ⊆ tᶜ

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

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

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

theorem Metric.AreSeparated.union_left {X : Type u_1} [PseudoEMetricSpace X] {s t s' : Set X} (h : AreSeparated s t) (h' : AreSeparated s' t) : AreSeparated (s ∪ s') t

@[simp]

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

theorem Metric.AreSeparated.union_right {X : Type u_1} [PseudoEMetricSpace X] {s t t' : Set X} (h : AreSeparated s t) (h' : AreSeparated s t') : AreSeparated s (t ∪ t')

@[simp]

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

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

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

Alias of the reverse direction of Metric.AreSeparated.finite_iUnion_left_iff.

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

@[simp]

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

theorem Metric.AreSeparated.finset_iUnion_left {X : Type u_1} [PseudoEMetricSpace X] {ι : Type u_2} {I : Finset ι} {s : ι → Set X} {t : Set X} : (∀ i ∈ I, AreSeparated (s i) t) → AreSeparated (⋃ i ∈ I, s i) t

Alias of the reverse direction of Metric.AreSeparated.finset_iUnion_left_iff.

@[simp]

theorem Metric.AreSeparated.finset_iUnion_right_iff {X : Type u_1} [PseudoEMetricSpace X] {ι : Type u_2} {I : Finset ι} {s : Set X} {t : ι → Set X} : AreSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, AreSeparated s (t i)

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

Alias of the reverse direction of Metric.AreSeparated.finset_iUnion_right_iff.