compCM — Mathlib

English

If g and f are continuous within a set s, then x ↦ g(x) ∘ f(x) is continuous within s at every point of s.

Русский

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

LaTeX

$$$\\text{ContinuousWithinAt } g\\,s\,a \\to \\text{ContinuousWithinAt } f\\,s\,a \\Rightarrow \\text{ContinuousWithinAt } (x\\mapsto g(x)\\circ f(x))\,s\,a$$$

Lean4

nonrec theorem _root_.ContinuousWithinAt.compCM (hg : ContinuousWithinAt g s a) (hf : ContinuousWithinAt f s a) :
    ContinuousWithinAt (fun x ↦ (g x).comp (f x)) s a :=
  hg.compCM hf

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