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
@[fun_prop]
theorem comp_inter {g : β → γ} {t : Set β} (hg : ContinuousOn g t) (hf : ContinuousOn f s) :
ContinuousOn (g ∘ f) (s ∩ f ⁻¹' t) :=
hg.comp (hf.mono inter_subset_left) inter_subset_right