map_of_continuousOn — Mathlib

English

If x specializes to y, f is ContinuousOn s, x ∈ s and y ∈ s, then f(x) specializes to f(y).

Русский

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

LaTeX

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

Lean4

theorem map_of_continuousOn {s : Set X} (h : x ⤳ y) (hf : ContinuousOn f s) (hx : x ∈ s) (hy : y ∈ s) : f x ⤳ f y :=
  h.map_of_continuousWithinAt (hf.continuousWithinAt hy) hx

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