map_of_continuousAt — Mathlib

English

If x specializes to y and f is ContinuousAt at y, then f(x) specializes to f(y).

Русский

Если x специализируется на y и f непрерывна в точке y, тогда f(x) специализируется на f(y).

LaTeX

$$$$\forall X\ Y, [\text{TopologicalSpace } X], [\text{TopologicalSpace } Y],\ {x,y:X}, {f:X\to Y},\ x\rightsquigarrow y \rightarrow ContinuousAt\ f\ y \rightarrow f\,x \rightsquigarrow f\,y.$$$$

Lean4

theorem map_of_continuousAt (h : x ⤳ y) (hf : ContinuousAt f y) : f x ⤳ f y :=
  h.map_of_continuousWithinAt hf.continuousWithinAt (mem_univ x)

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