cuspFunction_eq_of_nonzero

Mathlib.Analysis.Complex.Periodic

URI: https://scilib.ai/kg/mathlib#Function.Periodic.cuspFunction_eq_of_nonzero

English

If q ≠ 0, cuspFunction(h, f)(q) equals f(invQParam(h, q)).

Русский

Если q ≠ 0, cuspFunction(h, f)(q) равно f(invQParam(h, q)).

LaTeX

$$$q \neq 0 \Rightarrow cuspFunction(h,f)(q) = f(invQParam(h,q))$$$

Lean4

theorem cuspFunction_eq_of_nonzero {q : ℂ} (hq : q ≠ 0) : cuspFunction h f q = f (invQParam h q) :=
  update_of_ne hq ..

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

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

Разделы

Аффилиация

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