instCoeOutComplex

Mathlib.Analysis.Complex.UpperHalfPlane.Basic

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.instCoeOutComplex

English

There is a canonical CoeOut from the upper half-plane to the complex numbers, i.e., the inclusion ℍ → ℂ.

Русский

Существует каноническое отображение из ℍ в ℂ, т. е. вложение ℍ → ℂ.

LaTeX

$$$\text{CoeOut } \mathbb{H} \mathbb{C}$, i.e., the inclusion map $\mathbb{H} \hookrightarrow \mathbb{C}$.$$

Lean4

instance : CoeOut ℍ ℂ :=
  ⟨UpperHalfPlane.coe⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru