invOn_arg_exp

Mathlib.Analysis.SpecialFunctions.Complex.Circle

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

English

The pair (arg ∘ (↑), exp) yields an inverse pair on the domain Circle to range Ioc(-π, π).

Русский

Пара (arg ∘ включение, exp) образует частичную обратную пару между Circle и Ioc(-π, π).

LaTeX

$$$$\\text{InvOn}(\\arg \\circ (\\uparrow), \\exp, Ioc(-\\pi,\\pi), \\text{univ}).$$$$

Lean4

theorem invOn_arg_exp : InvOn (arg ∘ (↑)) exp (Ioc (-π) π) univ :=
  argPartialEquiv.symm.invOn

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

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

Разделы

Аффилиация

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