Theorems · Theorem · general topology

Metric.diam_union

∀ {α : Type u} {s : Set α} {x y : α} [inst : PseudoMetricSpace α] {t : Set α},
  x ∈ s → y ∈ t → Metric.diam (s ∪ t) ≤ Metric.diam s + dist x y + Metric.diam t

The diameter of a union is controlled by the sum of the diameters, and the distance between any two points in each of the sets. This lemma is true without any side condition, since it is obviously true if s ∪ t is unbounded.

Defined in

Mathlib.Topology.MetricSpace.Bounded

Cited by

2 results in Mathlib

Foundations

Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpace