ratio_of_trivial — Mathlib

English

If for all x,y we have edist x y ∈ {0, ∞}, then ratio f = 1 for any dilation class element f.

Русский

Если расстояние между любыми двумя точками тривиально равно 0 или бесконечности, то ratio f = 1 для любого элемента дилатации.

LaTeX

$$[DilationClass F α β] f : ratio f = 1$$

Lean4

theorem ratio_of_trivial [DilationClass F α β] (f : F) (h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞) : ratio f = 1 :=
  if_pos h

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