analyticOrderAt_neg — Mathlib

English

The order at z0 is unchanged by replacing f with -f.

Русский

Порядок в точке z0 не меняется при замене f на -f.

LaTeX

$$$\operatorname{analyticOrderAt}(-f) z_0 = \operatorname{analyticOrderAt} f z_0$$$

Lean4

@[simp]
theorem analyticOrderAt_neg : analyticOrderAt (-f) z₀ = analyticOrderAt f z₀ :=
  by
  by_cases hf : AnalyticAt 𝕜 f z₀
  · refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_
    simp only [natCast_le_analyticOrderAt, hf, hf.neg]
    exact (Equiv.neg _).exists_congr <| by simp [neg_eq_iff_eq_neg]
  · rw [analyticOrderAt_of_not_analyticAt hf, analyticOrderAt_of_not_analyticAt <| analyticAt_neg.not.2 hf]

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