dist_ghDist — Mathlib

English

The Gromov–Hausdorff distance between two spaces equals the distance computed from their representatives.

Русский

Расстояние Громова–Хаусдорфа между двумя пространствами равно расстоянию между их представителями.

LaTeX

$$dist(p,q) = ghDist(p.Rep, q.Rep).$$

Lean4

theorem dist_ghDist (p q : GHSpace) : dist p q = ghDist p.Rep q.Rep := by rw [ghDist, p.toGHSpace_rep, q.toGHSpace_rep]

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