comp_of_mem_nhdsWithin_image_of_eq

English

If f is continuous within s at x and g agrees with f on insert x s, then g is continuous within s at x.

Русский

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

LaTeX

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

Lean4

theorem comp_of_mem_nhdsWithin_image_of_eq {g : β → γ} {t : Set β} {y : β} (hg : ContinuousWithinAt g t y)
    (hf : ContinuousWithinAt f s x) (hs : t ∈ 𝓝[f '' s] y) (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x := by
  subst hy; exact hg.comp_of_mem_nhdsWithin_image hf hs

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