cast_analyticOrderNatAt — Mathlib

English

If analyticOrderAt f z0 is finite, then analyticOrderNatAt f z0 equals the cast of analyticOrderAt f z0 to ℕ.

Русский

Если порядок аналитичности в точке z0 конечен, то аналитический порядок в ℕ совпадает с приведением к ℕ порядкa аналитичности в z0.

LaTeX

$$$\text{analyticOrderNatAt } f z_0 = (analyticOrderAt f z_0).toNat$$$

Lean4

@[simp]
theorem cast_analyticOrderNatAt (hf : analyticOrderAt f z₀ ≠ ⊤) : analyticOrderNatAt f z₀ = analyticOrderAt f z₀ :=
  ENat.coe_toNat hf

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