diam_union' — Mathlib

English

If (s ∩ t) is nonempty, then diam(s ∪ t) ≤ diam(s) + diam(t).

Русский

Если пересечение s и t непусто, то diam(s ∪ t) ≤ diam(s) + diam(t).

LaTeX

$$$ (s \\cap t) \\neq \\varnothing \\Rightarrow \\operatorname{diam}(s \\cup t) \\le \\operatorname{diam}(s) + \\operatorname{diam}(t) $$$

Lean4

/-- If two sets intersect, the diameter of the union is bounded by the sum of the diameters. -/
theorem diam_union' {t : Set α} (h : (s ∩ t).Nonempty) : diam (s ∪ t) ≤ diam s + diam t :=
  by
  rcases h with ⟨x, ⟨xs, xt⟩⟩
  simpa using diam_union xs xt

Похожие утверждения