congr — Mathlib

English

If AnalyticWithinAt f s x holds and g equals f on s (EqOn g f s) and g x = f x, then AnalyticWithinAt g s x holds.

Русский

Если AnalyticWithinAt f на s в x, и g совпадает с f на s (EqOn g f s) и g(x)=f(x), то AnalyticWithinAt g s x действительно.

LaTeX

$$$\text{AnalyticWithinAt}_{\mathcal{K}}(f,s,x) \to (\text{EqOn}(g,f,s)) \to (g(x)=f(x)) \to \text{AnalyticWithinAt}_{\mathcal{K}}(g,s,x)$$$

Lean4

theorem congr {f g : E → F} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) (hs : EqOn g f s) (hx : g x = f x) :
    AnalyticWithinAt 𝕜 g s x :=
  hf.congr_of_eventuallyEq hs.eventuallyEq_nhdsWithin hx

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