ratioHom — Mathlib

English

If α is a nontrivial metric space, then for dilations g and f, the ratio of their composition equals the product of their ratios.

Русский

Если пространство α ненулевое (не тривиальное метрическое пространство), то для дилатаций g и f отношение композиции равно произведению отношений.

LaTeX

$$$\\operatorname{ratio}(g \\circ f) = \\operatorname{ratio}(g) \\cdot \\operatorname{ratio}(f)$$$

Lean4

/-- `Dilation.ratio` as a monoid homomorphism from `α →ᵈ α` to `ℝ≥0`. -/
@[simps]
def ratioHom : (α →ᵈ α) →* ℝ≥0 :=
  ⟨⟨ratio, ratio_one⟩, ratio_mul⟩

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