comp_of_preimage_mem_nhdsWithin_of_eq

English

Let f,g: X→Y, and s ⊆ X with x ∈ s. If f and g agree on a neighborhood of x relative to s, then continuity of f on s at x implies continuity of g on s at x.

Русский

Пусть f,g: X→Y, s ⊆ X и x ∈ s. Если f и g согласованы на окрестности x относительно s, то непрерывность f на s в x влечет непрерывность g на s в x.

LaTeX

$$$ (f=g\text{ on some }U\in 𝓝[x] \text{ with } U\subseteq s) \Rightarrow (ContinuousWithinAt f s x \Rightarrow ContinuousWithinAt g s x).$$$

Lean4

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

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