comp_continuousOn' — Mathlib

English

Let g be continuous and f be continuous on s. Then the form y ↦ g(f y) is continuous on s.

Русский

Пусть g непрерывна, а f непрерывна на s. Тогда функция y ↦ g(f(y)) непрерывна на s.

LaTeX

$$$\text{Continuous } g \;\to\; \text{ContinuousOn } f\, s \;\to\; \text{ContinuousOn } (\lambda y. g (f y)) \; s$$$

Lean4

/-- Variant of `Continuous.comp_continuousOn` using the form `fun y ↦ g (f y)`
instead of `g ∘ f`. -/
@[fun_prop]
theorem comp_continuousOn' {g : β → γ} {f : α → β} {s : Set α} (hg : Continuous g) (hf : ContinuousOn f s) :
    ContinuousOn (fun x ↦ g (f x)) s :=
  hg.comp_continuousOn hf

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