English
The diameter of a union is controlled by the sum of the diameters and the distance between the chosen points.
Русский
Диаметр объединения контролируется суммой диаметров и расстоянием между выбранными точками.
LaTeX
$$$\\operatorname{diam}(s \\cup t) \\le \\operatorname{diam}(s) + \\operatorname{dist}(x,y) + \\operatorname{diam}(t)$$$
Lean4
/-- 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. -/
theorem diam_union {t : Set α} (xs : x ∈ s) (yt : y ∈ t) : diam (s ∪ t) ≤ diam s + dist x y + diam t :=
by
simp only [diam, dist_edist]
refine (ENNReal.toReal_le_add' (EMetric.diam_union xs yt) ?_ ?_).trans (add_le_add_right ENNReal.toReal_add_le _)
· simp only [ENNReal.add_eq_top, edist_ne_top, or_false]
exact fun h ↦ top_unique <| h ▸ EMetric.diam_mono subset_union_left
· exact fun h ↦ top_unique <| h ▸ EMetric.diam_mono subset_union_right
