HepLean Documentation

Mathlib.Topology.EMetricSpace.Diam

Diameters of sets in extended metric spaces #

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

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

Equations
Instances For
    source
    theorem EMetric.diam_eq_sSup {α : Type u_1} [PseudoEMetricSpace α] (s : Set α) :
    EMetric.diam s = sSup (Set.image2 edist s s)
    source
    theorem EMetric.diam_le_iff {α : Type u_1} {s : Set α} [PseudoEMetricSpace α] {d : ENNReal} :
    EMetric.diam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d
    source
    theorem EMetric.diam_image_le_iff {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] {d : ENNReal} {f : β → α} {s : Set β} :
    EMetric.diam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d
    source
    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
    source
    theorem EMetric.edist_le_diam_of_mem {α : Type u_1} {s : Set α} {x y : α} [PseudoEMetricSpace α] (hx : x ∈ s) (hy : y ∈ s) :
    edist x y ≤ EMetric.diam s

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

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

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

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

    The diameter of a subsingleton vanishes.

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

    The diameter of the empty set vanishes

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

    The diameter of a singleton vanishes

    source
    @[simp]
    theorem EMetric.diam_one {α : Type u_1} [PseudoEMetricSpace α] [One α] :
    EMetric.diam 1 = 0
    source
    @[simp]
    theorem EMetric.diam_zero {α : Type u_1} [PseudoEMetricSpace α] [Zero α] :
    EMetric.diam 0 = 0
    source
    theorem EMetric.diam_iUnion_mem_option {α : Type u_1} [PseudoEMetricSpace α] {ι : Type u_3} (o : Option ι) (s : ι → Set α) :
    EMetric.diam (⋃ i ∈ o, s i) = ⨆ i ∈ o, EMetric.diam (s i)
    source
    theorem EMetric.diam_insert {α : Type u_1} {s : Set α} {x : α} [PseudoEMetricSpace α] :
    EMetric.diam (insert x s) = (⨆ y ∈ s, edist x y) ⊔ EMetric.diam s
    source
    theorem EMetric.diam_pair {α : Type u_1} {x y : α} [PseudoEMetricSpace α] :
    EMetric.diam {x, y} = edist x y
    source
    theorem EMetric.diam_triple {α : Type u_1} {x y z : α} [PseudoEMetricSpace α] :
    EMetric.diam {x, y, z} = edist x y ⊔ edist x z ⊔ edist y z
    source
    theorem EMetric.diam_mono {α : Type u_1} [PseudoEMetricSpace α] {s t : Set α} (h : s ⊆ t) :
    EMetric.diam s ≤ EMetric.diam t

    The diameter is monotonous with respect to inclusion

    source
    theorem EMetric.diam_union {α : Type u_1} {s : Set α} {x y : α} [PseudoEMetricSpace α] {t : Set α} (xs : x ∈ s) (yt : y ∈ t) :
    EMetric.diam (s ∪ t) ≤ EMetric.diam s + edist x y + EMetric.diam t

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

    source
    theorem EMetric.diam_union' {α : Type u_1} {s : Set α} [PseudoEMetricSpace α] {t : Set α} (h : (s ∩ t).Nonempty) :
    EMetric.diam (s ∪ t) ≤ EMetric.diam s + EMetric.diam t
    source
    theorem EMetric.diam_closedBall {α : Type u_1} {x : α} [PseudoEMetricSpace α] {r : ENNReal} :
    EMetric.diam (EMetric.closedBall x r) ≤ 2 * r
    source
    theorem EMetric.diam_ball {α : Type u_1} {x : α} [PseudoEMetricSpace α] {r : ENNReal} :
    EMetric.diam (EMetric.ball x r) ≤ 2 * r
    source
    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
    source
    theorem EMetric.diam_eq_zero_iff {β : Type u_2} [EMetricSpace β] {s : Set β} :
    EMetric.diam s = 0 ↔ s.Subsingleton
    source
    theorem EMetric.diam_pos_iff {β : Type u_2} [EMetricSpace β] {s : Set β} :
    0 < EMetric.diam s ↔ s.Nontrivial
    source
    theorem EMetric.diam_pos_iff' {β : Type u_2} [EMetricSpace β] {s : Set β} :
    0 < EMetric.diam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y