English
There exists an auxiliary metric on the upper half-plane that uses the standard distance from the ambient complex plane. This makes the upper half-plane a metric space with the usual metric axioms, and the distance being zero characterizes equality of points.
Русский
Существуют вспомогательная метрика на верхней полуплоскости и она задаётся обычным евклидовым расстоянием в плоскости, тем самым верхняя полуплоскость является метрическим пространством; расстояние нулю эквивалентно равенству точек.
LaTeX
$$$d(z,w) = |z-w|, \\quad z,w \\in \\mathbb{H};\\quad d \\text{ является метрикой на } \\mathbb{H},\\quad d(z,w)=0 \\iff z=w.$$$
Lean4
/-- An auxiliary `MetricSpace` instance on the upper half-plane. This instance has bad projection
to `TopologicalSpace`. We replace it later. -/
def metricSpaceAux : MetricSpace ℍ where
dist := dist
dist_self z := by rw [dist_eq, dist_self, zero_div, arsinh_zero, mul_zero]
dist_comm := UpperHalfPlane.dist_comm
dist_triangle := UpperHalfPlane.dist_triangle
eq_of_dist_eq_zero {z w}
h := by simpa [dist_eq, Real.sqrt_eq_zero', (mul_pos z.im_pos w.im_pos).not_ge, Set.ext_iff] using h
