congr_set — Mathlib

English

Let f be continuous within s at x. If s and t agree eventually near x (i.e., s is equal to t along a neighborhood of x in the sense of nhds x), then f is continuous within t at x.

Русский

Пусть f непрерывна на месте x относительно множества s. Если множества s и t совпадают в окрестности x, то f непрерывна на месте x относительно множества t.

LaTeX

$$$$\text{ContinuousWithinAt}(f,s,x) \land s =^{\mathcal{N}x}_{?} t \Rightarrow \text{ContinuousWithinAt}(f,t,x)$$$$

Lean4

theorem congr_set (hf : ContinuousWithinAt f s x) (h : s =ᶠ[𝓝 x] t) : ContinuousWithinAt f t x :=
  (continuousWithinAt_congr_set h).1 hf

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