# Diameters of sets in extended metric spaces #

source
noncomputable def EMetric.diam {α : Type u_1} [PseudoEMetricSpace α] (s : Set α) :
ENNReal

The diameter of a set in a pseudoemetric space, named `EMetric.diam`

Equations

- EMetric.diam s = ⨆ x ∈ s, ⨆ y ∈ s, edist x y

Instances For

source
theorem EMetric.diam_eq_sSup {α : Type u_1} [PseudoEMetricSpace α] (s : Set α) :
diam s = sSup (Set.image2 edist s s)
source
theorem EMetric.diam_le_iff {α : Type u_1} {s : Set α} [PseudoEMetricSpace α] {d : ENNReal} :
diam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d
source
theorem EMetric.diam_image_le_iff {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] {d : ENNReal} {f : β → α} {s : Set β} :
diam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d
source
theorem EMetric.edist_le_of_diam_le {α : Type u_1} {s : Set α} {x y : α} [PseudoEMetricSpace α] {d : ENNReal} (hx : x ∈ s) (hy : y ∈ s) (hd : diam s ≤ d) :
edist x y ≤ d
source
theorem EMetric.edist_le_diam_of_mem {α : Type u_1} {s : Set α} {x y : α} [PseudoEMetricSpace α] (hx : x ∈ s) (hy : y ∈ s) :
edist x y ≤ diam s

If two points belong to some set, their edistance is bounded by the diameter of the set

source
theorem EMetric.diam_le {α : Type u_1} {s : Set α} [PseudoEMetricSpace α] {d : ENNReal} (h : ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d) :
diam s ≤ d

If the distance between any two points in a set is bounded by some constant, this constant bounds the diameter.

source
theorem EMetric.diam_subsingleton {α : Type u_1} {s : Set α} [PseudoEMetricSpace α] (hs : s.Subsingleton) :
diam s = 0

The diameter of a subsingleton vanishes.

source
@[simp]
theorem EMetric.diam_empty {α : Type u_1} [PseudoEMetricSpace α] :
diam ∅ = 0

The diameter of the empty set vanishes

source
@[simp]
theorem EMetric.diam_singleton {α : Type u_1} {x : α} [PseudoEMetricSpace α] :
diam {x} = 0

The diameter of a singleton vanishes

source
@[simp]
theorem EMetric.diam_one {α : Type u_1} [PseudoEMetricSpace α] [One α] :
diam 1 = 0
source
@[simp]
theorem EMetric.diam_zero {α : Type u_1} [PseudoEMetricSpace α] [Zero α] :
diam 0 = 0
source
theorem EMetric.diam_iUnion_mem_option {α : Type u_1} [PseudoEMetricSpace α] {ι : Type u_3} (o : Option ι) (s : ι → Set α) :
diam (⋃ i ∈ o, s i) = ⨆ i ∈ o, diam (s i)
source
theorem EMetric.diam_insert {α : Type u_1} {s : Set α} {x : α} [PseudoEMetricSpace α] :
diam (insert x s) = max (⨆ y ∈ s, edist x y) (diam s)
source
theorem EMetric.diam_pair {α : Type u_1} {x y : α} [PseudoEMetricSpace α] :
diam {x, y} = edist x y
source
theorem EMetric.diam_triple {α : Type u_1} {x y z : α} [PseudoEMetricSpace α] :
diam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)
source
theorem EMetric.diam_mono {α : Type u_1} [PseudoEMetricSpace α] {s t : Set α} (h : s ⊆ t) :
diam s ≤ diam t

The diameter is monotonous with respect to inclusion

source
theorem EMetric.diam_union {α : Type u_1} {s : Set α} {x y : α} [PseudoEMetricSpace α] {t : Set α} (xs : x ∈ s) (yt : y ∈ t) :
diam (s ∪ t) ≤ diam s + edist x y + diam t

The diameter of a union is controlled by the diameter of the sets, and the edistance between two points in the sets.

source
theorem EMetric.diam_union' {α : Type u_1} {s : Set α} [PseudoEMetricSpace α] {t : Set α} (h : (s ∩ t).Nonempty) :
diam (s ∪ t) ≤ diam s + diam t
source
theorem EMetric.diam_closedBall {α : Type u_1} {x : α} [PseudoEMetricSpace α] {r : ENNReal} :
diam (closedBall x r) ≤ 2 * r
source
theorem EMetric.diam_ball {α : Type u_1} {x : α} [PseudoEMetricSpace α] {r : ENNReal} :
diam (ball x r) ≤ 2 * r
source
theorem EMetric.diam_pi_le_of_le {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoEMetricSpace (X b)] {s : (b : β) → Set (X b)} {c : ENNReal} (h : ∀ (b : β), diam (s b) ≤ c) :
diam (Set.univ.pi s) ≤ c
source
theorem EMetric.diam_eq_zero_iff {β : Type u_2} [EMetricSpace β] {s : Set β} :
diam s = 0 ↔ s.Subsingleton
source
theorem EMetric.diam_pos_iff {β : Type u_2} [EMetricSpace β] {s : Set β} :
0 < diam s ↔ s.Nontrivial
source
theorem EMetric.diam_pos_iff' {β : Type u_2} [EMetricSpace β] {s : Set β} :
0 < diam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y