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