analyticAt_congr — Mathlib

English

For any f,g and x, if f =ᶠ[𝓝 x] g, then AnalyticAt 𝕜 f x ⇔ AnalyticAt 𝕜 g x.

Русский

Если f эквивалентна g почти в окрестности x, тогда аналитичность в x равносильна между f и g.

LaTeX

$$$\text{AnalyticAt}_{\mathcal{K}}(f,x) \iff \text{AnalyticAt}_{\mathcal{K}}(g,x)$ при $f =^\!_{\mathcal{N} x} g$$$

Lean4

theorem analyticAt_congr (h : f =ᶠ[𝓝 x] g) : AnalyticAt 𝕜 f x ↔ AnalyticAt 𝕜 g x :=
  ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩

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