Diameters of sets in extended metric spaces #
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
theorem
EMetric.diam_image_le_iff
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
{d : ENNReal}
{f : β → α}
{s : Set β}
:
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]
The diameter of a singleton vanishes
theorem
EMetric.diam_iUnion_mem_option
{α : Type u_1}
[PseudoEMetricSpace α]
{ι : Type u_3}
(o : Option ι)
(s : ι → Set α)
:
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)
: