mono_of_mem_nhdsWithin — Mathlib

English

If a function f is analytic within s, then any g which is eventually equal to f on the neighborhood inside insert x s is analytic within s.

Русский

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

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 mono_of_mem_nhdsWithin (h : AnalyticWithinAt 𝕜 f s x) (hst : s ∈ 𝓝[t] x) : AnalyticWithinAt 𝕜 f t x :=
  by
  rcases h with ⟨p, hp⟩
  exact ⟨p, hp.mono_of_mem_nhdsWithin hst⟩

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