English
The extended diameter of the image equals ratio times the extended diameter of the original set.
Русский
Удлинённая диаметр изображения равен отношению дилатации, умноженному на удлинённую диаметр исходного множества.
LaTeX
$$$\\operatorname{ediam}\\big( f[S] \\big) = \\operatorname{ratio}(f) \\cdot \\operatorname{ediam}(S)$$$
Lean4
/-- Dilations scale the diameter by `ratio f` in pseudoemetric spaces. -/
theorem ediam_image (s : Set α) : EMetric.diam ((f : α → β) '' s) = ratio f * EMetric.diam s :=
by
refine ((lipschitz f).ediam_image_le s).antisymm ?_
apply ENNReal.mul_le_of_le_div'
rw [div_eq_mul_inv, mul_comm, ← ENNReal.coe_inv]
exacts [(antilipschitz f).le_mul_ediam_image s, ratio_ne_zero f]
