map — Mathlib

English

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

Русский

Если x специализируется на y и f непрерывна, тогда 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 Continuous f \rightarrow f\,x \rightsquigarrow f\,y.$$$$

Lean4

theorem map (h : x ⤳ y) (hf : Continuous f) : f x ⤳ f y :=
  h.map_of_continuousAt hf.continuousAt

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