congr_of_eventuallyEq_insert — Mathlib

English

Let f,g: X→Y, s⊆X, x∈s. If f is continuous within s at x and g equals f on insert x s near x (i.e., g =ᶠ[𝓝[insert x s] x] f), then g is continuous within s at x.

Русский

Пусть f,g: X→Y, s⊆X, x∈s. Если f непрерывна на s в x и g совпадает с f в окрестности x внутри insert x s, тогда g непрерывна на s в x.

LaTeX

$$$ \text{Let } f,g: X\to Y,\ s\subseteq X,\ x\in s.\ (∃ U\in 𝓝[\mathrm{insert}\ x\ s] x:\ U\subseteq \mathrm{insert}\ x\ s\land \forall y\in U\ g(y)=f(y))\Rightarrow\ ContinuousWithinAt(g,s,x).$$$

Lean4

theorem congr_of_eventuallyEq_insert (h : ContinuousWithinAt f s x) (h₁ : g =ᶠ[𝓝[insert x s] x] f) :
    ContinuousWithinAt g s x :=
  h.congr_of_eventuallyEq (nhdsWithin_mono _ (subset_insert _ _) h₁) (mem_of_mem_nhdsWithin (mem_insert _ _) h₁ :)

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