comp_inter_of_eq — Mathlib

English

Let g be continuous on t, f continuous on s. If y = f(x) and hy: f x = y, then g∘f is continuous at x on s.

Русский

Пусть g непрерывна на t, f непрерывна на s. Пусть y = f(x) и hy: f x = y. Тогда g∘f непрерывна в x на s.

LaTeX

$$$ (ContinuousOn g t) \land (ContinuousOn f s) \land (f x = y) \Rightarrow ContinuousWithinAt (g\circ f) s x . $$$

Lean4

theorem comp_inter_of_eq {g : β → γ} {t : Set β} {y : β} (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x)
    (hy : f x = y) : ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x := by subst hy; exact hg.comp_inter hf

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