comp_of_mem_nhdsWithin_image — Mathlib

English

If g agrees with f on insert x s relative to s, then continuity of f on s at x implies continuity of g on s at x.

Русский

Если g совпадает с f на вставке x s относительно s, то непрерывность f на s в x влечет непрерывность g на s в x.

LaTeX

$$$ (f\text{ continuous within } s\; x) \land (g =^{𝓝[\mathrm{insert}\ x\ s]} f) \Rightarrow (ContinuousWithinAt g s x).$$$

Lean4

theorem comp_of_mem_nhdsWithin_image {g : β → γ} {t : Set β} (hg : ContinuousWithinAt g t (f x))
    (hf : ContinuousWithinAt f s x) (hs : t ∈ 𝓝[f '' s] f x) : ContinuousWithinAt (g ∘ f) s x :=
  (hg.mono_of_mem_nhdsWithin hs).comp hf (mapsTo_image f s)

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