image_comp_continuous — Mathlib

English

If g is continuous on a set s, and f is continuous, and f maps into s, then the composition g ∘ f is continuous on the domain.

Русский

Пусть g непрерывна на s, f непрерывна и образ f лежит в s; тогда g ∘ f непрерывна на домене.

LaTeX

$$$\text{ContinuousOn } g\, s \;\to\; \text{Continuous } f \;\to\; (\forall x, f(x) \in s) \;\to\; \text{Continuous } (g \circ f)$$$

Lean4

theorem image_comp_continuous {g : β → γ} {f : α → β} {s : Set α} (hg : ContinuousOn g (f '' s)) (hf : Continuous f) :
    ContinuousOn (g ∘ f) s :=
  hg.comp hf.continuousOn (s.mapsTo_image f)

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