diam_triple — Mathlib

English

The diameter of {x,y,z} is the maximum of the pairwise distances: max(max(dist(x,y), dist(x,z)), dist(y,z)).

Русский

Диаметр множества {x,y,z} равен максимуму попарных расстояний: max(max(dist(x,y), dist(x,z)), dist(y,z)).

LaTeX

$$$\\operatorname{diam}(\\{x,y,z\\}) = \\max\\big(\\max(\\operatorname{dist}(x,y), \\operatorname{dist}(x,z)), \\operatorname{dist}(y,z)\\big)$$$

Lean4

theorem diam_triple : Metric.diam ({ x, y, z } : Set α) = max (max (dist x y) (dist x z)) (dist y z) :=
  by
  simp only [Metric.diam, EMetric.diam_triple, dist_edist]
  rw [ENNReal.toReal_max, ENNReal.toReal_max] <;> apply_rules [ne_of_lt, edist_lt_top, max_lt]

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