Diameters of sets in extended metric spaces #

In this file we define the diameter of a set in the extended metric space as an extended nonnegative real number.

source

noncomputable def Metric.ediam {X : Type u_2} [PseudoEMetricSpace X] (s : Set X) :

ENNReal

The diameter of a set in a pseudoemetric space as an extended nonnegative real number.

Equations

Metric.ediam s = ⨆ x ∈ s, ⨆ y ∈ s, edist x y

Instances For

source

theorem Metric.ediam_eq_sSup {X : Type u_2} [PseudoEMetricSpace X] (s : Set X) :

ediam s = sSup (Set.image2 edist s s)

source

theorem Metric.ediam_le_iff {X : Type u_2} {s : Set X} [PseudoEMetricSpace X] {d : ENNReal} :

ediam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d

source

theorem Metric.ediam_image_le_iff {α : Type u_1} {X : Type u_2} [PseudoEMetricSpace X] {d : ENNReal} {f : α → X} {s : Set α} :

ediam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d

source

theorem Metric.edist_le_of_ediam_le {X : Type u_2} {s : Set X} {x y : X} [PseudoEMetricSpace X] {d : ENNReal} (hx : x ∈ s) (hy : y ∈ s) (hd : ediam s ≤ d) :

edist x y ≤ d

source

theorem Metric.edist_le_ediam_of_mem {X : Type u_2} {s : Set X} {x y : X} [PseudoEMetricSpace X] (hx : x ∈ s) (hy : y ∈ s) :

edist x y ≤ ediam s

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

source

theorem Metric.ediam_le {X : Type u_2} {s : Set X} [PseudoEMetricSpace X] {d : ENNReal} (h : ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d) :

ediam s ≤ d

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

source

theorem Metric.ediam_subsingleton {X : Type u_2} {s : Set X} [PseudoEMetricSpace X] (hs : s.Subsingleton) :

ediam s = 0

The diameter of a subsingleton vanishes.

source

theorem Set.Subsingleton.ediam_eq {X : Type u_2} {s : Set X} [PseudoEMetricSpace X] (hs : s.Subsingleton) :

Metric.ediam s = 0

Alias of Metric.ediam_subsingleton.

The diameter of a subsingleton vanishes.

source

@[simp]

theorem Metric.ediam_empty {X : Type u_2} [PseudoEMetricSpace X] :

ediam ∅ = 0

The diameter of the empty set vanishes

source

@[simp]

theorem Metric.ediam_singleton {X : Type u_2} {x : X} [PseudoEMetricSpace X] :

ediam {x} = 0

The extended diameter of a singleton vanishes

source

@[simp]

theorem Metric.ediam_one {X : Type u_2} [PseudoEMetricSpace X] [One X] :

ediam 1 = 0

source

@[simp]

theorem Metric.ediam_zero {X : Type u_2} [PseudoEMetricSpace X] [Zero X] :

ediam 0 = 0

source

theorem Metric.ediam_iUnion_mem_option {X : Type u_2} [PseudoEMetricSpace X] {ι : Type u_3} (o : Option ι) (s : ι → Set X) :

ediam (⋃ i ∈ o, s i) = ⨆ i ∈ o, ediam (s i)

source

theorem Metric.ediam_insert {X : Type u_2} {s : Set X} {x : X} [PseudoEMetricSpace X] :

ediam (insert x s) = max (⨆ y ∈ s, edist x y) (ediam s)

source

theorem Metric.ediam_pair {X : Type u_2} {x y : X} [PseudoEMetricSpace X] :

ediam {x, y} = edist x y

source

theorem Metric.ediam_triple {X : Type u_2} {x y z : X} [PseudoEMetricSpace X] :

ediam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)

source

theorem Metric.ediam_mono {X : Type u_2} {s t : Set X} [PseudoEMetricSpace X] (h : s ⊆ t) :

ediam s ≤ ediam t

The extended diameter is monotonous with respect to inclusion

source

theorem Metric.ediam_union_le_add_edist {X : Type u_2} {s t : Set X} {x y : X} [PseudoEMetricSpace X] (xs : x ∈ s) (yt : y ∈ t) :

ediam (s ∪ t) ≤ ediam s + edist x y + ediam t

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

source

theorem Metric.ediam_union_le {X : Type u_2} {s t : Set X} [PseudoEMetricSpace X] (h : (s ∩ t).Nonempty) :

ediam (s ∪ t) ≤ ediam s + ediam t

If two sets have nonempty intersection, then the extended diameter of their union is estimated from above by the sum of their union.

source

theorem Metric.ediam_closedEBall_le {X : Type u_2} {x : X} [PseudoEMetricSpace X] {r : ENNReal} :

ediam (EMetric.closedBall x r) ≤ 2 * r

source

theorem Metric.ediam_eball_le {X : Type u_2} {x : X} [PseudoEMetricSpace X] {r : ENNReal} :

ediam (EMetric.ball x r) ≤ 2 * r

source

theorem Metric.ediam_pi_le_of_le {ι : Type u_3} {X : ι → Type u_4} [Fintype ι] [(i : ι) → PseudoEMetricSpace (X i)] {s : (i : ι) → Set (X i)} {c : ENNReal} (h : ∀ (b : ι), ediam (s b) ≤ c) :

ediam (Set.univ.pi s) ≤ c

source

theorem Metric.ediam_eq_zero_iff {X : Type u_2} {s : Set X} [EMetricSpace X] :

ediam s = 0 ↔ s.Subsingleton

source

theorem Metric.ediam_pos_iff {X : Type u_2} {s : Set X} [EMetricSpace X] :

0 < ediam s ↔ s.Nontrivial

source

theorem Metric.ediam_pos_iff' {X : Type u_2} {s : Set X} [EMetricSpace X] :

0 < ediam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y

source

@[deprecated Metric.ediam (since := "2026-01-04")]

def EMetric.diam {X : Type u_2} [PseudoEMetricSpace X] (s : Set X) :

ENNReal

Alias of Metric.ediam.

The diameter of a set in a pseudoemetric space as an extended nonnegative real number.

Equations

@EMetric.diam = @Metric.ediam

Instances For

source

@[deprecated Metric.ediam_eq_sSup (since := "2026-01-04")]

theorem EMetric.diam_eq_sSup {X : Type u_2} [PseudoEMetricSpace X] (s : Set X) :

Metric.ediam s = sSup (Set.image2 edist s s)

Alias of Metric.ediam_eq_sSup.

source

@[deprecated Metric.ediam_le_iff (since := "2026-01-04")]

theorem EMetric.diam_le_iff {X : Type u_2} {s : Set X} [PseudoEMetricSpace X] {d : ENNReal} :

Metric.ediam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d

Alias of Metric.ediam_le_iff.

source

@[deprecated Metric.ediam_image_le_iff (since := "2026-01-04")]

theorem EMetric.diam_image_le_iff {α : Type u_1} {X : Type u_2} [PseudoEMetricSpace X] {d : ENNReal} {f : α → X} {s : Set α} :

Metric.ediam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d

Alias of Metric.ediam_image_le_iff.

source

@[deprecated Metric.edist_le_of_ediam_le (since := "2026-01-04")]

theorem EMetric.edist_le_of_diam_le {X : Type u_2} {s : Set X} {x y : X} [PseudoEMetricSpace X] {d : ENNReal} (hx : x ∈ s) (hy : y ∈ s) (hd : Metric.ediam s ≤ d) :

edist x y ≤ d

Alias of Metric.edist_le_of_ediam_le.

source

@[deprecated Metric.edist_le_ediam_of_mem (since := "2026-01-04")]

theorem EMetric.edist_le_diam_of_mem {X : Type u_2} {s : Set X} {x y : X} [PseudoEMetricSpace X] (hx : x ∈ s) (hy : y ∈ s) :

edist x y ≤ Metric.ediam s

Alias of Metric.edist_le_ediam_of_mem.

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

source

@[deprecated Metric.ediam_le (since := "2026-01-04")]

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

Metric.ediam s ≤ d

Alias of Metric.ediam_le.

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

source

@[deprecated Metric.ediam_subsingleton (since := "2026-01-04")]

theorem EMetric.diam_subsingleton {X : Type u_2} {s : Set X} [PseudoEMetricSpace X] (hs : s.Subsingleton) :

Metric.ediam s = 0

Alias of Metric.ediam_subsingleton.

The diameter of a subsingleton vanishes.

source

@[deprecated Metric.ediam_empty (since := "2026-01-04")]

theorem EMetric.diam_empty {X : Type u_2} [PseudoEMetricSpace X] :

Metric.ediam ∅ = 0

Alias of Metric.ediam_empty.

The diameter of the empty set vanishes

source

@[deprecated Metric.ediam_singleton (since := "2026-01-04")]

theorem EMetric.diam_singleton {X : Type u_2} {x : X} [PseudoEMetricSpace X] :

Metric.ediam {x} = 0

Alias of Metric.ediam_singleton.

The extended diameter of a singleton vanishes

source

@[deprecated Metric.ediam_zero (since := "2026-01-04")]

theorem EMetric.diam_zero {X : Type u_2} [PseudoEMetricSpace X] [Zero X] :

Metric.ediam 0 = 0

Alias of Metric.ediam_zero.

source

@[deprecated Metric.ediam_one (since := "2026-01-04")]

theorem EMetric.diam_one {X : Type u_2} [PseudoEMetricSpace X] [One X] :

Metric.ediam 1 = 0

Alias of Metric.ediam_one.

source

@[deprecated Metric.ediam_iUnion_mem_option (since := "2026-01-04")]

theorem EMetric.diam_iUnion_mem_option {X : Type u_2} [PseudoEMetricSpace X] {ι : Type u_3} (o : Option ι) (s : ι → Set X) :

Metric.ediam (⋃ i ∈ o, s i) = ⨆ i ∈ o, Metric.ediam (s i)

Alias of Metric.ediam_iUnion_mem_option.

source

@[deprecated Metric.ediam_insert (since := "2026-01-04")]

theorem EMetric.diam_insert {X : Type u_2} {s : Set X} {x : X} [PseudoEMetricSpace X] :

Metric.ediam (insert x s) = max (⨆ y ∈ s, edist x y) (Metric.ediam s)

Alias of Metric.ediam_insert.

source

@[deprecated Metric.ediam_pair (since := "2026-01-04")]

theorem EMetric.diam_pair {X : Type u_2} {x y : X} [PseudoEMetricSpace X] :

Metric.ediam {x, y} = edist x y

Alias of Metric.ediam_pair.

source

@[deprecated Metric.ediam_triple (since := "2026-01-04")]

theorem EMetric.diam_triple {X : Type u_2} {x y z : X} [PseudoEMetricSpace X] :

Metric.ediam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)

Alias of Metric.ediam_triple.

source

@[deprecated Metric.ediam_mono (since := "2026-01-04")]

theorem EMetric.diam_mono {X : Type u_2} {s t : Set X} [PseudoEMetricSpace X] (h : s ⊆ t) :

Metric.ediam s ≤ Metric.ediam t

Alias of Metric.ediam_mono.

The extended diameter is monotonous with respect to inclusion

source

@[deprecated Metric.ediam_union_le_add_edist (since := "2026-01-04")]

theorem EMetric.diam_union {X : Type u_2} {s t : Set X} {x y : X} [PseudoEMetricSpace X] (xs : x ∈ s) (yt : y ∈ t) :

Metric.ediam (s ∪ t) ≤ Metric.ediam s + edist x y + Metric.ediam t

Alias of Metric.ediam_union_le_add_edist.

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

source

@[deprecated Metric.ediam_union_le (since := "2026-01-04")]

theorem EMetric.diam_union' {X : Type u_2} {s t : Set X} [PseudoEMetricSpace X] (h : (s ∩ t).Nonempty) :

Metric.ediam (s ∪ t) ≤ Metric.ediam s + Metric.ediam t

Alias of Metric.ediam_union_le.

If two sets have nonempty intersection, then the extended diameter of their union is estimated from above by the sum of their union.

source

@[deprecated Metric.ediam_closedEBall_le (since := "2026-01-04")]

theorem EMetric.diam_closedBall {X : Type u_2} {x : X} [PseudoEMetricSpace X] {r : ENNReal} :

Metric.ediam (closedBall x r) ≤ 2 * r

Alias of Metric.ediam_closedEBall_le.

source

@[deprecated Metric.ediam_eball_le (since := "2026-01-04")]

theorem EMetric.diam_ball {X : Type u_2} {x : X} [PseudoEMetricSpace X] {r : ENNReal} :

Metric.ediam (ball x r) ≤ 2 * r

Alias of Metric.ediam_eball_le.

source

@[deprecated Metric.ediam_pi_le_of_le (since := "2026-01-04")]

theorem EMetric.diam_pi_le_of_le {ι : Type u_3} {X : ι → Type u_4} [Fintype ι] [(i : ι) → PseudoEMetricSpace (X i)] {s : (i : ι) → Set (X i)} {c : ENNReal} (h : ∀ (b : ι), Metric.ediam (s b) ≤ c) :

Metric.ediam (Set.univ.pi s) ≤ c

Alias of Metric.ediam_pi_le_of_le.

source

@[deprecated Metric.ediam_eq_zero_iff (since := "2026-01-04")]