analyticOnNhd_congr' — Mathlib

English

If IsOpen s and s.EqOn f g, then AnalyticOnNhd 𝕜 f s ↔ AnalyticOnNhd 𝕜 g s.

Русский

При открытом s и равенстве функций на s, аналитичность на окрестности совпадает.

LaTeX

$$$\text{IsOpen}(s) \land s.EqOn(f,g) \Rightarrow \text{AnalyticOnNhd}_{\mathcal{K}}(f,s) \iff \text{AnalyticOnNhd}_{\mathcal{K}}(g,s)$$$

Lean4

theorem analyticOnNhd_congr' (h : f =ᶠ[𝓝ˢ s] g) : AnalyticOnNhd 𝕜 f s ↔ AnalyticOnNhd 𝕜 g s :=
  ⟨fun hf => hf.congr' h, fun hg => hg.congr' h.symm⟩

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