Documentation

Mathlib.Topology.EMetricSpace.Diam

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
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 (closedEBall x r) ≤ 2 * r
    source
    theorem Metric.ediam_eball_le {X : Type u_2} {x : X} [PseudoEMetricSpace X] {r : ENNReal} :
    ediam (eball 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