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.

def IsMetricSeparated {X : Type u_1} [EMetricSpace X] (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} [EMetricSpace X] {s : Set X} {t : Set X} (h : IsMetricSeparated s t) :
    theorem IsMetricSeparated.disjoint {X : Type u_1} [EMetricSpace X] {s : Set X} {t : Set X} (h : IsMetricSeparated s t) :
    theorem IsMetricSeparated.subset_compl_right {X : Type u_1} [EMetricSpace X] {s : Set X} {t : Set X} (h : IsMetricSeparated s t) :
    s t
    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') :
    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') :
    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') :
    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) :
    @[simp]
    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') :
    @[simp]
    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 (⋃ iI, s i) t iI, 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} :
    (∀ 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} [EMetricSpace X] {ι : 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} [EMetricSpace X] {ι : Type u_2} {I : Finset ι} {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} [EMetricSpace X] {ι : Type u_2} {I : Finset ι} {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} [EMetricSpace X] {ι : Type u_2} {I : Finset ι} {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} [EMetricSpace X] {ι : Type u_2} {I : Finset ι} {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.