continuousAt_congr — Mathlib

English

Let f and g be maps X → Y and suppose f is eventually equal to g near x, i.e. f =ᶠ[𝓝 x] g. Then f is continuous at x if and only if g is continuous at x.

Русский

Пусть f и g: X → Y. Если f и g совпадают в окрестности x (f =ᶠ[𝓝 x] g), то непрерывность f в x эквивалентна непрерывности g в x.

LaTeX

$$$f =^\\!{\\mathcal{N}_x} g \\\\Rightarrow \\\\big( \\mathrm{ContinuousAt}(f, x) \\iff \\mathrm{ContinuousAt}(g, x) \\big)$$$

Lean4

theorem continuousAt_congr {g : X → Y} (h : f =ᶠ[𝓝 x] g) : ContinuousAt f x ↔ ContinuousAt g x := by
  simp only [ContinuousAt, tendsto_congr' h, h.eq_of_nhds]

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