congr' — Mathlib

English

If an analytic on neighborhood (AnalyticOnNhd) f is defined on t and s ⊆ t, then f is analytic on s as well.

Русский

Если аналитичность в окрестности f определена на t и s ⊆ t, то она сохраняется на s.

LaTeX

$$$\text{AnalyticOnNhd}_{\mathcal{K}}(f,t) \land s \subseteq t \Rightarrow \text{AnalyticOnNhd}_{\mathcal{K}}(f,s)$$$

Lean4

theorem congr' (hf : AnalyticOnNhd 𝕜 f s) (hg : f =ᶠ[𝓝ˢ s] g) : AnalyticOnNhd 𝕜 g s := fun z hz =>
  (hf z hz).congr (mem_nhdsSet_iff_forall.mp hg z hz)

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