Documentation

Mathlib.Topology.MetricSpace.MetricSeparated

Metric separated pairs of sets #

In this file 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.

source
def Metric.AreSeparated {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
Instances For
    source
    @[deprecated Metric.AreSeparated (since := "2025-01-21")]
    def Metric.IsMetricSeparated {X : Type u_1} [EMetricSpace X] (s t : Set X) :
    Prop

    Alias of Metric.AreSeparated.

    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
      source
      theorem Metric.AreSeparated.symm {X : Type u_1} [EMetricSpace X] {s t : Set X} (h : AreSeparated s t) :
      AreSeparated t s
      source
      theorem Metric.AreSeparated.comm {X : Type u_1} [EMetricSpace X] {s t : Set X} :
      AreSeparated s t ↔ AreSeparated t s
      source
      @[simp]
      theorem Metric.AreSeparated.empty_left {X : Type u_1} [EMetricSpace X] (s : Set X) :
      AreSeparated ∅ s
      source
      @[simp]
      theorem Metric.AreSeparated.empty_right {X : Type u_1} [EMetricSpace X] (s : Set X) :
      AreSeparated s ∅
      source
      theorem Metric.AreSeparated.disjoint {X : Type u_1} [EMetricSpace X] {s t : Set X} (h : AreSeparated s t) :
      Disjoint s t
      source
      theorem Metric.AreSeparated.subset_compl_right {X : Type u_1} [EMetricSpace X] {s t : Set X} (h : AreSeparated s t) :
      s ⊆ tᶜ
      source
      theorem Metric.AreSeparated.mono {X : Type u_1} [EMetricSpace X] {s t s' t' : Set X} (hs : s ⊆ s') (ht : t ⊆ t') :
      AreSeparated s' t' → AreSeparated s t
      source
      theorem Metric.AreSeparated.mono_left {X : Type u_1} [EMetricSpace X] {s t s' : Set X} (h' : AreSeparated s' t) (hs : s ⊆ s') :
      AreSeparated s t
      source
      theorem Metric.AreSeparated.mono_right {X : Type u_1} [EMetricSpace X] {s t t' : Set X} (h' : AreSeparated s t') (ht : t ⊆ t') :
      AreSeparated s t
      source
      theorem Metric.AreSeparated.union_left {X : Type u_1} [EMetricSpace X] {s t s' : Set X} (h : AreSeparated s t) (h' : AreSeparated s' t) :
      AreSeparated (s ∪ s') t
      source
      @[simp]
      theorem Metric.AreSeparated.union_left_iff {X : Type u_1} [EMetricSpace X] {s t s' : Set X} :
      AreSeparated (s ∪ s') t ↔ AreSeparated s t ∧ AreSeparated s' t
      source
      theorem Metric.AreSeparated.union_right {X : Type u_1} [EMetricSpace X] {s t t' : Set X} (h : AreSeparated s t) (h' : AreSeparated s t') :
      AreSeparated s (t ∪ t')
      source
      @[simp]
      theorem Metric.AreSeparated.union_right_iff {X : Type u_1} [EMetricSpace X] {s t t' : Set X} :
      AreSeparated s (t ∪ t') ↔ AreSeparated s t ∧ AreSeparated s t'
      source
      theorem Metric.AreSeparated.finite_iUnion_left_iff {X : Type u_1} [EMetricSpace 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
      source
      theorem Metric.AreSeparated.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, AreSeparated (s i) t) → AreSeparated (⋃ i ∈ I, s i) t

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

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

      source
      @[simp]
      theorem Metric.AreSeparated.finset_iUnion_right_iff {X : Type u_1} [EMetricSpace X] {ι : Type u_2} {I : Finset ι} {s : Set X} {t : ι → Set X} :
      AreSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, AreSeparated s (t i)
      source
      theorem Metric.AreSeparated.finset_iUnion_right {X : Type u_1} [EMetricSpace 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.