instCoeOut — Mathlib

English

There is a natural inclusion map sending each point of the unit circle into the complex plane, i.e., Circle embeds into ℂ.

Русский

Существует естественное вложение, отображающее каждую точку единичной окружности в точку на плоскости ℂ.

LaTeX

$$$$ \\iota: \\ Circle \\hookrightarrow \\mathbb{C}, \\quad \\iota(z) = z. $$$$

Lean4

instance instCoeOut : CoeOut Circle ℂ :=
  subtypeCoe

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