ratio_id — Mathlib

English

The ratio of the identity dilation on any space is equal to 1.

Русский

Соотношение дилатации — тождественной на любой пространстве равно единице.

LaTeX

$$$\\operatorname{ratio}(\\mathrm{Id}_\\alpha) = 1$$$

Lean4

theorem ratio_id : ratio (Dilation.id α) = 1 :=
  by
  by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
  · rw [ratio, if_pos h]
  · push_neg at h
    rcases h with ⟨x, y, hne⟩
    refine (ratio_unique hne.1 hne.2 ?_).symm
    simp

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