English
If f is continuous at y, g,h are continuous within s at x, and y = (g x, h x), then f(g x, h x) is continuous within s at x.
Русский
Если f непрерывна в точке y, а g,h непрерывны внутри s в x, и y = (g x, h x), то f(g x, h x) непрерывна внутри s в x.
LaTeX
$$$\text{ContinuousAt } f y \to \text{ContinuousWithinAt } g\ s\ x \to \text{ContinuousWithinAt } h\ s\ x \to \text{Eq } {\text{fst}}{\text{snd}} y \to \text{ContinuousWithinAt } (\lambda x. f (g x, h x))\ s\ x$$$
Lean4
theorem comp₂_continuousWithinAt_of_eq {f : β × γ → δ} {g : α → β} {h : α → γ} {x : α} {s : Set α} {y : β × γ}
(hf : ContinuousAt f y) (hg : ContinuousWithinAt g s x) (hh : ContinuousWithinAt h s x) (e : (g x, h x) = y) :
ContinuousWithinAt (fun x ↦ f (g x, h x)) s x :=
by
rw [← e] at hf
exact hf.comp₂_continuousWithinAt hg hh
