congr — Mathlib

English

If f is analytic at x and f and g are equal almost everywhere near x, then g is analytic at x as well.

Русский

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

LaTeX

$$$\text{AnalyticAt}_{\mathcal{K}}(f,x) \land (f =^\!_{\mathcal{N} x} g) \Rightarrow \text{AnalyticAt}_{\mathcal{K}}(g,x)$$$

Lean4

theorem congr (hf : AnalyticAt 𝕜 f x) (hg : f =ᶠ[𝓝 x] g) : AnalyticAt 𝕜 g x :=
  let ⟨_, hpf⟩ := hf
  (hpf.congr hg).analyticAt

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