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

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

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 : I.Finite) {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 : 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.

source

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)

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.

Documentation

Mathlib.Topology.MetricSpace.MetricSeparated

Metric separated pairs of sets #