diam_insert — Mathlib

English

The diameter of the union with a point x and a set s is the maximum of the distance from x to s and the diameter of s.

Русский

Диаметр множества, полученного добавлением точки x к s, равен максимуму между расстоянием от x до s и диаметром s.

LaTeX

$$\operatorname{diam}(\operatorname{insert} x\, s) = \max\left( \bigvee_{y \in s} \operatorname{edist}(x,y), \operatorname{diam}(s) \right)$$

Lean4

theorem diam_insert : diam (insert x s) = max (⨆ y ∈ s, edist x y) (diam s) :=
  eq_of_forall_ge_iff fun d => by
    simp only [diam_le_iff, forall_mem_insert, edist_self, edist_comm x, max_le_iff, iSup_le_iff, zero_le, true_and,
      forall_and, and_self_iff, ← and_assoc]

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