congr_continuousWithinAt — Mathlib

English

If f and g are equal on s in nhds, then ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x; similarly for the reverse direction.

Русский

Если f и g равны на s в окрестностях x, то ContinuousWithinAt f s x ⇔ ContinuousWithinAt g s x; и наоборот.

LaTeX

$$$$ (\text{nhdsWithin } x s).\text{EventuallyEq } f g \Rightarrow (\text{ContinuousWithinAt}(f,s,x) \iff \text{ContinuousWithinAt}(g,s,x)) $$$$

Lean4

theorem congr_continuousWithinAt (h : f =ᶠ[𝓝[s] x] g) (hx : f x = g x) :
    ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x := by
  rw [ContinuousWithinAt, hx, tendsto_congr' h, ContinuousWithinAt]

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