congr_continuousWithinAt_of_insert

English

Let f,g: X→Y, s⊆X, x∈s. If g equals f on insert x s near x, then g is continuous within s at x if f is.

Русский

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

LaTeX

$$$ \text{If } (\forall y\in \mathrm{insert}\ x\ s,\ g(y)=f(y)) \Rightarrow (\text{ContinuousWithinAt}(g,s,x) \iff \text{ContinuousWithinAt}(f,s,x)).$$$

Lean4

theorem congr_continuousWithinAt_of_insert (h : f =ᶠ[𝓝[insert x s] x] g) :
    ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x :=
  ⟨fun h' ↦ h'.congr_of_eventuallyEq_insert h.symm, fun h' ↦ h'.congr_of_eventuallyEq_insert h⟩

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