instChartedSpaceComplex — Mathlib

English

The upper half-plane ℍ carries a charted space structure compatible with the complex plane via the coe map.

Русский

Верхняя полуплоскость ℍ имеет структуру charted space, совместимую с комплексной плоскостью через отображение включения.

LaTeX

$$$\text{UpperHalfPlane.instChartedSpaceComplex}$$$

Lean4

noncomputable instance : ChartedSpace ℂ ℍ :=
  UpperHalfPlane.isOpenEmbedding_coe.singletonChartedSpace

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