Documentation

Mathlib.Topology.EMetricSpace.Diam

Diameters of sets in extended metric spaces #

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

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

Equations
theorem EMetric.diam_eq_sSup {α : Type u_1} [PseudoEMetricSpace α] (s : Set α) :
theorem EMetric.diam_le_iff {α : Type u_1} {s : Set α} [PseudoEMetricSpace α] {d : ENNReal} :
EMetric.diam s d xs, ys, edist x y d
theorem EMetric.diam_image_le_iff {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] {d : ENNReal} {f : βα} {s : Set β} :
EMetric.diam (f '' s) d xs, ys, 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 : EMetric.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) :

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 : xs, ys, edist x y 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) :

The diameter of a subsingleton vanishes.

@[simp]

The diameter of the empty set vanishes

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

The diameter of a singleton vanishes

@[simp]
theorem EMetric.diam_zero {α : Type u_1} [PseudoEMetricSpace α] [Zero α] :
@[simp]
theorem EMetric.diam_one {α : Type u_1} [PseudoEMetricSpace α] [One α] :
theorem EMetric.diam_iUnion_mem_option {α : Type u_1} [PseudoEMetricSpace α] {ι : Type u_3} (o : Option ι) (s : ιSet α) :
EMetric.diam (⋃ io, s i) = io, EMetric.diam (s i)
theorem EMetric.diam_insert {α : Type u_1} {s : Set α} {x : α} [PseudoEMetricSpace α] :
EMetric.diam (insert x s) = max (⨆ ys, edist x y) (EMetric.diam s)
theorem EMetric.diam_pair {α : Type u_1} {x : α} {y : α} [PseudoEMetricSpace α] :
EMetric.diam {x, y} = edist x y
theorem EMetric.diam_triple {α : Type u_1} {x : α} {y : α} {z : α} [PseudoEMetricSpace α] :
EMetric.diam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)
theorem EMetric.diam_mono {α : Type u_1} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (h : s 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) :

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) :
theorem EMetric.diam_ball {α : Type u_1} {x : α} [PseudoEMetricSpace α] {r : ENNReal} :
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 : β), EMetric.diam (s b) c) :
EMetric.diam (Set.univ.pi s) c
theorem EMetric.diam_eq_zero_iff {β : Type u_2} [EMetricSpace β] {s : Set β} :
EMetric.diam s = 0 s.Subsingleton
theorem EMetric.diam_pos_iff {β : Type u_2} [EMetricSpace β] {s : Set β} :
0 < EMetric.diam s s.Nontrivial
theorem EMetric.diam_pos_iff' {β : Type u_2} [EMetricSpace β] {s : Set β} :
0 < EMetric.diam s xs, ys, x y