congr — Mathlib

English

If f is analytic on s (AnalyticOn 𝕜 f s) and g agrees with f on s (EqOn g f s), then g is analytic on s (AnalyticOn 𝕜 g s).

Русский

Если f аналитична на s и g совпадает с f на s, тогда g аналитична на s.

LaTeX

$$$\text{AnalyticOn}_{\mathcal{K}}(f,s) \land \text{EqOn}_{s}(g,f) \Rightarrow \text{AnalyticOn}_{\mathcal{K}}(g,s)$$$

Lean4

theorem congr {f g : E → F} {s : Set E} (hf : AnalyticOn 𝕜 f s) (hs : EqOn g f s) : AnalyticOn 𝕜 g s := fun x m ↦
  (hf x m).congr hs (hs m)

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