congr_continuousWithinAt_of_mem — Mathlib

English

Let f,g: X→Y and s⊆X with x∈s. If f is continuous within s at x and g equals f on a neighborhood of x within s, then f is continuous within s at x if and only if g is.

Русский

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

LaTeX

$$$ \text{Let } f,g: X\to Y,\ s\subseteq X,\ x\in s.\ (f\text{ continuous within } s\ x) \iff (g\text{ continuous within } s\ x)$, provided $g=f$ on some $U\in\mathcal{N}(x)$ with $U\subseteq s$.$$

Lean4

theorem congr_continuousWithinAt_of_mem (h : f =ᶠ[𝓝[s] x] g) (hx : x ∈ s) :
    ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x :=
  ⟨fun h' ↦ h'.congr_of_eventuallyEq_of_mem h.symm hx, fun h' ↦ h'.congr_of_eventuallyEq_of_mem h hx⟩

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