congr — Mathlib

English

If (nhdsSet s).EventuallyEq f g, then AnalyticOnNhd 𝕜 f s ↔ AnalyticOnNhd 𝕜 g s.

Русский

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

LaTeX

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

Lean4

theorem congr (hs : IsOpen s) (hf : AnalyticOnNhd 𝕜 f s) (hg : s.EqOn f g) : AnalyticOnNhd 𝕜 g s :=
  hf.congr' <| mem_nhdsSet_iff_forall.mpr (fun _ hz => eventuallyEq_iff_exists_mem.mpr ⟨s, hs.mem_nhds hz, hg⟩)

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