congr_of_eventuallyEq — Mathlib

English

If f is analytic within s at x, and g agrees with f on s near x (g =ᶠ[𝓝[s] x] f) and g(x) = f(x), then g is analytic within s at x.

Русский

Если f аналитична внутри s в точке x, и g совпадает с f на окрестности x внутри s (g =ᶠ[𝓝[s] x] f) и g(x) = f(x), тогда g аналитична внутри s в x.

LaTeX

$$$\text{AnalyticWithinAt}_{\mathcal{K}}(f,s,x) \land (g =^\!\!_{\mathcal{N}\!hdsWithin[s] x} f) \land (g(x)=f(x)) \Rightarrow \text{AnalyticWithinAt}_{\mathcal{K}}(g,s,x)$$$

Lean4

theorem congr_of_eventuallyEq {f g : E → F} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) (hs : g =ᶠ[𝓝[s] x] f)
    (hx : g x = f x) : AnalyticWithinAt 𝕜 g s x :=
  by
  rcases hf with ⟨p, hp⟩
  exact ⟨p, hp.congr hs hx⟩

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