Documentation

Mathlib.Topology.MetricSpace.MetricSeparated

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.

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

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

    source
    @[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)
    source
    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.