English
In a classical metric space, the ratio of the composition equals the product of ratios.
Русский
В классическом метрическом пространстве отношение композиции равно произведению отношений.
LaTeX
$$$\\operatorname{ratio}(g \\circ f) = \\operatorname{ratio}(g) \\cdot \\operatorname{ratio}(f)$$$
Lean4
/-- Ratio of the composition `g.comp f` of two dilations is the product of their ratios. We assume
that the domain `α` of `f` is a nontrivial metric space, otherwise
`Dilation.ratio f = Dilation.ratio (g.comp f) = 1` but `Dilation.ratio g` may have any value.
See also `Dilation.ratio_comp'` for a version that works for more general spaces. -/
@[simp]
theorem ratio_comp [MetricSpace α] [Nontrivial α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {g : β →ᵈ γ}
{f : α →ᵈ β} : ratio (g.comp f) = ratio g * ratio f :=
ratio_comp' <|
let ⟨x, y, hne⟩ := exists_pair_ne α;
⟨x, y, mt edist_eq_zero.1 hne, edist_ne_top _ _⟩
