congr_of_eventuallyEq — Mathlib

English

If f and g are eventually equal near x within s, and f is continuous within s at x, then g is continuous within s at x.

Русский

Если f и g равны почти повсюду рядом с x внутри s, и f непрерывна на s в x, тогда g непрерывна на s в x.

LaTeX

$$$$\text{ContinuousWithinAt}(f,s,x) \land (f =^\!_{\mathcal{N}[s]x} g) \Rightarrow \text{ContinuousWithinAt}(g,s,x)$$$$

Lean4

theorem congr_of_eventuallyEq (h : ContinuousWithinAt f s x) (h₁ : g =ᶠ[𝓝[s] x] f) (hx : g x = f x) :
    ContinuousWithinAt g s x :=
  (h₁.congr_continuousWithinAt hx).2 h

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