English
The Hausdorff distance between the optimal left and right image ranges is at most the HD distance of any candidate.
Русский
Расстояние Хаусдорфа между оптимальными изображениями слева и справа не больше HD любого кандидата.
LaTeX
$$hausdorffDist( range(optimalGHInjl X Y), range(optimalGHInjr X Y)) \le HD f$$
Lean4
/-- Unfold the definition of `dimH` using `[MeasurableSpace X] [BorelSpace X]` from the
environment. -/
theorem dimH_def (s : Set X) : dimH s = ⨆ (d : ℝ≥0) (_ : μH[d] s = ∞), (d : ℝ≥0∞) := by borelize X; rw [dimH]