comp_continuousOn — Mathlib

English

Let g be continuous, and f be continuous on a set s. Then the composition g ∘ f is continuous on s.

Русский

Пусть g непрерывна, а f непрерывна на множестве s. Тогда композиция g ∘ f непрерывна на s.

LaTeX

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

Lean4

/-- See also `Continuous.comp_continuousOn'` using the form `fun y ↦ g (f y)`
instead of `g ∘ f`. -/
theorem comp_continuousOn {g : β → γ} {f : α → β} {s : Set α} (hg : Continuous g) (hf : ContinuousOn f s) :
    ContinuousOn (g ∘ f) s :=
  hg.continuousOn.comp hf (mapsTo_univ _ _)

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