ratio_mul — Mathlib

English

Same as ratio_comp' for g and f: the ratio of the composition equals the product of the ratios, under the same hypothesis.

Русский

То же, что и для ratio_comp' для 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

@[simp]
theorem ratio_mul (f g : α →ᵈ α) : ratio (f * g) = ratio f * ratio g :=
  by
  by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
  · simp [ratio_of_trivial, h]
  push_neg at h
  exact ratio_comp' h

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