comp_continuousWithinAt_of_eq — Mathlib

English

If g is continuous at y, f is continuous within s at x, and f(x)=y, then g∘f is continuous within s at x.

Русский

Если g непрерывна в y, f непрерывна на s в x и f(x)=y, то g∘f непрерывна на s в x.

LaTeX

$$$ (ContinuousAt g y) \land (ContinuousWithinAt f s x) \land (f x = y) \Rightarrow ContinuousWithinAt (g\circ f) s x.$$$

Lean4

theorem comp_continuousWithinAt_of_eq {g : β → γ} {y : β} (hg : ContinuousAt g y) (hf : ContinuousWithinAt f s x)
    (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x := by subst hy; exact hg.comp_continuousWithinAt hf

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