diam_union' — Mathlib

English

If s and t have a nonempty intersection, then diam(s ∪ t) ≤ diam(s) + diam(t).

Русский

Если пересечение s и t непусто, то диаметр объединения diam(s ∪ t) ≤ diam(s) + diam(t).

LaTeX

$$\operatorname{diam}(s \cup t) \le \operatorname{diam}(s) + \operatorname{diam}(t) \quad ( (s \cap t) \neq \emptyset )$$

Lean4

theorem diam_union' {t : Set α} (h : (s ∩ t).Nonempty) : diam (s ∪ t) ≤ diam s + diam t :=
  by
  let ⟨x, ⟨xs, xt⟩⟩ := h
  simpa using diam_union xs xt

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