comp — Mathlib

English

Let g: β→γ be continuous on t, f: α→β be continuous on s, and MapsTo f s t. Then g∘f is continuous on s.

Русский

Пусть g: β→γ непрерывна на t, f: α→β непрерывна на s, и f сохраняет отображение s в t. Тогда g∘f непрерывна на s.

LaTeX

$$$ (ContinuousOn g t) \land (ContinuousOn f s) \land (MapsTo f s t) \Rightarrow (ContinuousOn (g\circ f) s).$$$

Lean4

theorem comp {g : β → γ} {t : Set β} (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x)
    (h : MapsTo f s t) : ContinuousWithinAt (g ∘ f) s x :=
  hg.tendsto.comp (hf.tendsto_nhdsWithin h)

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