English
If g is continuous on t and f is continuous on s and MapsTo f s t, then the composed function x ↦ g(f(x)) is continuous on s.
Русский
Если g непрерывна на t и f непрерывна на s и MapsTo f s t, то x ↦ g(f(x)) непрерывна на s.
LaTeX
$$$ (ContinuousOn g t) \land (ContinuousOn f s) \land (MapsTo f s t) \Rightarrow ContinuousOn (fun x => g (f x)) s.$$$
Lean4
/-- Variant of `ContinuousOn.comp` using the form `fun y ↦ g (f y)` instead of `g ∘ f`. -/
@[fun_prop]
theorem comp' {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : ContinuousOn g t) (hf : ContinuousOn f s)
(h : Set.MapsTo f s t) : ContinuousOn (fun x => g (f x)) s :=
ContinuousOn.comp hg hf h
