English
For two dilations g and f, the ratio of their composition equals the product of their ratios, provided there exist two points at finite nonzero extended distance.
Русский
Для дилатаций g и f отношение композиции равно произведению их отношений, при условии существования двух точек на конечном ненулевом расстоянии.
LaTeX
$$$\\left( \\exists x,y\\in \\alpha, edist(x,y) \\neq 0 \\land edist(x,y) \\neq \\infty \\right) \\Rightarrow \\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 there exist two points in `α` at extended distance neither `0` nor `∞` because otherwise
`Dilation.ratio (g.comp f) = Dilation.ratio f = 1` while `Dilation.ratio g` can be any number. This
version works for most general spaces, see also `Dilation.ratio_comp` for a version assuming that
`α` is a nontrivial metric space. -/
theorem ratio_comp' {g : β →ᵈ γ} {f : α →ᵈ β} (hne : ∃ x y : α, edist x y ≠ 0 ∧ edist x y ≠ ⊤) :
ratio (g.comp f) = ratio g * ratio f := by
rcases hne with ⟨x, y, hα⟩
have hgf := (edist_eq (g.comp f) x y).symm
simp_rw [coe_comp, Function.comp, edist_eq, ← mul_assoc, ENNReal.mul_left_inj hα.1 hα.2] at hgf
rwa [← ENNReal.coe_inj, ENNReal.coe_mul]
