ediam_mul_le — Mathlib

English

Same as 54270: the diameter of the product is bounded by sum of diameters.

Русский

То же, что и в 54270: диаметр произведения ограничен суммой диаметров.

LaTeX

$$$\operatorname{ediam}(x y) \le \operatorname{ediam}(x) + \operatorname{ediam}(y)$$$

Lean4

@[to_additive]
theorem ediam_mul_le (x y : Set E) : EMetric.diam (x * y) ≤ EMetric.diam x + EMetric.diam y :=
  (LipschitzOnWith.ediam_image2_le (· * ·) _ _ (fun _ _ => (isometry_mul_right _).lipschitz.lipschitzOnWith) fun _ _ =>
        (isometry_mul_left _).lipschitz.lipschitzOnWith).trans_eq <|
    by simp only [ENNReal.coe_one, one_mul]

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