Diameters of sets in extended metric spaces

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

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

theorem EMetric.diam_eq_sSup {α : Type u_1} [PseudoEMetricSpace α] (s : Set α) : diam s = sSup (Set.image2 edist s s)

theorem EMetric.diam_le_iff {α : Type u_1} {s : Set α} [PseudoEMetricSpace α] {d : ENNReal} : diam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d

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

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

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

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.

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

The diameter of a subsingleton vanishes.

@[simp]

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

The diameter of the empty set vanishes

@[simp]

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

The diameter of a singleton vanishes

@[simp]

theorem EMetric.diam_one {α : Type u_1} [PseudoEMetricSpace α] [One α] : diam 1 = 0

@[simp]

theorem EMetric.diam_zero {α : Type u_1} [PseudoEMetricSpace α] [Zero α] : diam 0 = 0

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)

theorem EMetric.diam_insert {α : Type u_1} {s : Set α} {x : α} [PseudoEMetricSpace α] : diam (insert x s) = max (⨆ y ∈ s, edist x y) (diam s)

theorem EMetric.diam_pair {α : Type u_1} {x y : α} [PseudoEMetricSpace α] : diam {x, y} = edist x y

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)

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

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.

theorem EMetric.diam_union' {α : Type u_1} {s : Set α} [PseudoEMetricSpace α] {t : Set α} (h : (s ∩ t).Nonempty) : diam (s ∪ t) ≤ diam s + diam t

theorem EMetric.diam_closedBall {α : Type u_1} {x : α} [PseudoEMetricSpace α] {r : ENNReal} : diam (closedBall x r) ≤ 2 * r

theorem EMetric.diam_ball {α : Type u_1} {x : α} [PseudoEMetricSpace α] {r : ENNReal} : diam (ball x r) ≤ 2 * r

theorem EMetric.diam_pi_le_of_le {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoEMetricSpace (π b)] {s : (b : β) → Set (π b)} {c : ENNReal} (h : ∀ (b : β), diam (s b) ≤ c) : diam (Set.univ.pi s) ≤ c

theorem EMetric.diam_eq_zero_iff {β : Type u_2} [EMetricSpace β] {s : Set β} : diam s = 0 ↔ s.Subsingleton

theorem EMetric.diam_pos_iff {β : Type u_2} [EMetricSpace β] {s : Set β} : 0 < diam s ↔ s.Nontrivial

theorem EMetric.diam_pos_iff' {β : Type u_2} [EMetricSpace β] {s : Set β} : 0 < diam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y