comp_continuousWithinAt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem comp_continuousWithinAt {g : β → γ} (hg : ContinuousAt g (f x)) (hf : ContinuousWithinAt f s x) :
    ContinuousWithinAt (g ∘ f) s x :=
  hg.continuousWithinAt.comp hf (mapsTo_univ _ _)

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