analyticOnNhd_congr — Mathlib

English

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

Русский

Если s открыто и s.EqOn f g, аналитичность на окрестности совпадает.

LaTeX

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

Lean4

theorem analyticOnNhd_congr (hs : IsOpen s) (h : s.EqOn f g) : AnalyticOnNhd 𝕜 f s ↔ AnalyticOnNhd 𝕜 g s :=
  ⟨fun hf => hf.congr hs h, fun hg => hg.congr hs h.symm⟩

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