coe_injective — Mathlib

English

The natural inclusion from Circle to ℂ is injective; different points on the circle have different complex coordinates.

Русский

Естественное вложение окружности в ℂ инъективно; разные точки окружности имеют разные комплексные координаты.

LaTeX

$$$$ \\forall x,y \\in \\mathbb{S}^1, \\ (x \\uparrow) = (y \\uparrow) \\Rightarrow x = y. $$$$

Lean4

theorem coe_injective : Injective ((↑) : Circle → ℂ) := fun _ _ ↦ ext

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