comp_of_eq — Mathlib

English

If g is continuous on t and f is continuous on s, then g∘f is continuous on s ∩ f^{-1}(t).

Русский

Если g непрерывна на t, а f непрерывна на s, то g∘f непрерывна на s ∩ f^{-1}(t).

LaTeX

$$$ (ContinuousOn g t) \land (ContinuousOn f s) \Rightarrow ContinuousOn (g\circ f) (s\cap f^{-1}(t)).$$$

Lean4

theorem comp_of_eq {g : β → γ} {t : Set β} {y : β} (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x)
    (h : MapsTo f s t) (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x := by subst hy; exact hg.comp hf h

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