analyticOrderAt_of_not_analyticAt

Mathlib.Analysis.Analytic.Order

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

English

If f is not analytic at z0, then analyticOrderNatAt f z0 = 0.

Русский

Если функция не аналитична в точке z0, то analyticOrderNatAt f z0 = 0.

LaTeX

$$$\text{analyticOrderNatAt } f z_0 = 0$$$

Lean4

@[simp]
theorem analyticOrderAt_of_not_analyticAt (hf : ¬AnalyticAt 𝕜 f z₀) : analyticOrderAt f z₀ = 0 :=
  dif_neg hf

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

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

Разделы

Аффилиация

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