infEdist_inv_inv — Mathlib

English

The diameter of a product of two sets is at most the sum of the diameters.

Русский

Диаметр произведения множеств не превосходит суммы диаметров.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem infEdist_inv_inv (x : E) (s : Set E) : infEdist x⁻¹ s⁻¹ = infEdist x s := by
  rw [← image_inv_eq_inv, infEdist_image isometry_inv]

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