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
theorem
EMetric.diam_eq_sSup
{α : Type u_1}
[PseudoEMetricSpace α]
(s : Set α)
:
EMetric.diam s = sSup (Set.image2 edist s s)
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
theorem
EMetric.diam_image_le_iff
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
{d : ENNReal}
{f : β → α}
{s : Set β}
:
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)
:
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
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.
theorem
EMetric.diam_subsingleton
{α : Type u_1}
{s : Set α}
[PseudoEMetricSpace α]
(hs : s.Subsingleton)
:
EMetric.diam s = 0
The diameter of a subsingleton vanishes.
@[simp]
The diameter of the empty set vanishes
@[simp]
The diameter of a singleton vanishes
@[simp]
@[simp]
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)
theorem
EMetric.diam_insert
{α : Type u_1}
{s : Set α}
{x : α}
[PseudoEMetricSpace α]
:
EMetric.diam (insert x s) = max (⨆ y ∈ s, 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_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)
:
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.
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
theorem
EMetric.diam_closedBall
{α : Type u_1}
{x : α}
[PseudoEMetricSpace α]
{r : ENNReal}
:
EMetric.diam (EMetric.closedBall x r) ≤ 2 * r
theorem
EMetric.diam_ball
{α : Type u_1}
{x : α}
[PseudoEMetricSpace α]
{r : ENNReal}
:
EMetric.diam (EMetric.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 : β), 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 ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y