injective_arg

Mathlib.Analysis.SpecialFunctions.Complex.Circle

URI: https://scilib.ai/kg/mathlib#Circle.injective_arg

English

The map z ↦ arg z is injective on the unit circle.

Русский

Отображение z ↦ arg z на единичной окружности инъективно.

LaTeX

$$$$\\forall z,w \\in \\mathbb{C}, |z|=1, |w|=1: \\ arg z = \\ arg w \\Rightarrow z = w.$$$$

Lean4

theorem injective_arg : Injective fun z : Circle => arg z := fun z w h =>
  Subtype.ext <| ext_norm_arg (z.norm_coe.trans w.norm_coe.symm) h

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

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

Разделы

Аффилиация

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