congr_of_eventuallyEq_insert — Mathlib

English

If AnalyticWithinAt f within s holds, and g equals f eventually on the neighborhood of x within insert x s, then AnalyticWithinAt g s x holds.

Русский

Если AnalyticWithinAt f внутри s выполняется в точке x, и g совпадает с f почти повсюду в окрестности x внутри вставки x s, тогда AnalyticWithinAt g внутри s в x выполняется.

LaTeX

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

Lean4

theorem congr_of_eventuallyEq_insert {f g : E → F} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x)
    (hs : g =ᶠ[𝓝[insert x s] x] f) : AnalyticWithinAt 𝕜 g s x :=
  by
  apply hf.congr_of_eventuallyEq (nhdsWithin_mono x (subset_insert x s) hs)
  apply mem_of_mem_nhdsWithin (mem_insert x s) hs

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