comp_continuous — Mathlib

English

If g is continuous on s and f is continuous, and f maps into s, then g ∘ f is continuous.

Русский

Если 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 comp_continuous {g : β → γ} {f : α → β} {s : Set β} (hg : ContinuousOn g s) (hf : Continuous f)
    (hs : ∀ x, f x ∈ s) : Continuous (g ∘ f) :=
  by
  rw [← continuousOn_univ] at *
  exact hg.comp hf fun x _ => hs x

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