English
The hyperbolic metric on the upper half-plane is defined so that the projection to the standard topology matches the subtype topology of the upper half-plane.
Русский
Гиперболическая метрика на верхней полуплоскости задаётся так, что проекция на стандартную топологию совпадает с топологией подтипа верхней полуплоскости.
LaTeX
$$$\\text{There exists a MetricSpace structure on } \\mathbb{H} \\text{ with the induced topology equal to the subspace topology from } \\mathbb{C}.$$$
Lean4
/-- The hyperbolic metric on the upper half plane. We ensure that the projection to
`TopologicalSpace` is definitionally equal to the subtype topology. -/
instance : MetricSpace ℍ :=
metricSpaceAux.replaceTopology <| by
refine le_antisymm (continuous_id_iff_le.1 ?_) ?_
· refine (@continuous_iff_continuous_dist ℍ ℍ metricSpaceAux.toPseudoMetricSpace _ _).2 ?_
have : ∀ x : ℍ × ℍ, 2 * √(x.1.im * x.2.im) ≠ 0 := fun x => by
positivity
-- `continuity` fails to apply `Continuous.div`
apply_rules [Continuous.div, Continuous.mul, continuous_const, Continuous.arsinh, Continuous.dist,
continuous_coe.comp, continuous_fst, continuous_snd, Real.continuous_sqrt.comp, continuous_im.comp]
· letI : MetricSpace ℍ := metricSpaceAux
refine le_of_nhds_le_nhds fun z => ?_
rw [nhds_induced]
refine (nhds_basis_ball.le_basis_iff (nhds_basis_ball.comap _)).2 fun R hR => ?_
have h₁ : 1 < R / im z + 1 := lt_add_of_pos_left _ (div_pos hR z.im_pos)
have h₀ : 0 < R / im z + 1 := one_pos.trans h₁
refine ⟨log (R / im z + 1), Real.log_pos h₁, ?_⟩
refine fun w hw => (dist_coe_le w z).trans_lt ?_
rwa [← lt_div_iff₀' z.im_pos, sub_lt_iff_lt_add, ← Real.lt_log_iff_exp_lt h₀]
