circleMap_neg_radius

Mathlib.MeasureTheory.Integral.CircleIntegral

URI: https://scilib.ai/kg/mathlib#circleMap_neg_radius

English

For any r,x ∈ ℝ and c ∈ ℂ, circleMap(c, −r, x) = circleMap(c, r, x + π).

Русский

Для любых r,x ∈ ℝ и c ∈ ℂ выполняется circleMap(c, −r, x) = circleMap(c, r, x + π).

LaTeX

$$$ circleMap(c,-r,x) = circleMap(c,r,x+\pi). $$$

Lean4

theorem circleMap_neg_radius {r x : ℝ} {c : ℂ} : circleMap c (-r) x = circleMap c r (x + π) := by
  simp [circleMap, add_mul, Complex.exp_add]

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

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

Разделы

Аффилиация

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