ediam_image — Mathlib

English

Isometries preserve the diameter of sets in pseudoemetric spaces: diam(f[S]) = diam(S).

Русский

Изометрии сохраняют диаметр множества: диаметр образа равен диаметру множества.

LaTeX

$$$\forall s:\, EMetric.diam( f''s ) = EMetric.diam(s)$$$

Lean4

/-- Isometries preserve the diameter in pseudoemetric spaces. -/
theorem ediam_image (hf : Isometry f) (s : Set α) : EMetric.diam (f '' s) = EMetric.diam s :=
  eq_of_forall_ge_iff fun d => by simp only [EMetric.diam_le_iff, forall_mem_image, hf.edist_eq]

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