comp — Mathlib

English

If g is continuous on t, f is continuous on s, and MapsTo f s t, then g∘f is continuous on s.

Русский

Если g непрерывна на t, f непрерывна на s, и MapsTo f s t, то g∘f непрерывна на s.

LaTeX

$$$ (ContinuousOn g t) \land (ContinuousOn f s) \land (MapsTo f s t) \Rightarrow ContinuousOn (Function\,.{\} g f) s.$$$

Lean4

/-- See also `ContinuousOn.comp'` using the form `fun y ↦ g (f y)` instead of `g ∘ f`. -/
theorem comp {g : β → γ} {t : Set β} (hg : ContinuousOn g t) (hf : ContinuousOn f s) (h : MapsTo f s t) :
    ContinuousOn (g ∘ f) s := fun x hx => ContinuousWithinAt.comp (hg _ (h hx)) (hf x hx) h

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