ediam_range — Mathlib

English

The extended diameter of the range equals ratio times the extended diameter of the whole space.

Русский

Удлинённая диаметр образа равен отношению дилатации умноженному на диаметр всего пространства.

LaTeX

$$$\\operatorname{ediam}(\\operatorname{range}(f)) = \\operatorname{ratio}(f) \\cdot \\operatorname{ediam}(\\operatorname{univ})$$$

Lean4

/-- A dilation scales the diameter of the range by `ratio f`. -/
theorem ediam_range : EMetric.diam (range (f : α → β)) = ratio f * EMetric.diam (univ : Set α) := by rw [← image_univ];
  exact ediam_image f univ

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