analyticOrderNatAt_of_not_analyticAt

English

If f is analytic at z0, analyticOrderNatAt f z0 = n is equivalent to the local representation f z = (z - z0)^n g z with g analytic and nonvanishing at z0.

Русский

Если f аналитична в z0, то analyticOrderNatAt f z0 = n эквивалентно существованию локального представления f z = (z - z0)^n g z, где g аналитично и не обращается в нуль в z0.

LaTeX

$$$\text{analyticOrderNatAt } f z_0 = n \iff \exists g \, (\text{AnalyticAt } 𝕜 g z_0) \wedge g z_0 \neq 0 \wedge \forall^\nhds z_0, f z = (z - z_0)^n g z$$$

Lean4

@[simp]
theorem analyticOrderNatAt_of_not_analyticAt (hf : ¬AnalyticAt 𝕜 f z₀) : analyticOrderNatAt f z₀ = 0 := by
  simp [analyticOrderNatAt, hf]

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