English
The ratio of the composition equals the product of the ratios.
Русский
Отношение композиции равно произведению отношений.
LaTeX
$$$\\operatorname{ratio}(g \\circ f) = \\operatorname{ratio}(g) \\cdot \\operatorname{ratio}(f)$$$
Lean4
/-- A dilation maps balls to balls and scales the radius by `ratio f`. -/
theorem mapsTo_emetric_ball (x : α) (r : ℝ≥0∞) :
MapsTo (f : α → β) (EMetric.ball x r) (EMetric.ball (f x) (ratio f * r)) := fun y hy =>
(edist_eq f y x).trans_lt <|
(ENNReal.mul_lt_mul_left (ENNReal.coe_ne_zero.2 <| ratio_ne_zero f) ENNReal.coe_ne_top).2 hy