compCM — Mathlib

English

If g and f are continuous on a set s, then x ↦ g(x) ∘ f(x) is continuous on s.

Русский

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

LaTeX

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

Lean4

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

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