English
If f is continuous within s at x and g is continuous within s at x, then x ↦ (f x, g x) is continuous within s at x.
Русский
Если f и g непрерывны внутри s в x, то x ↦ (f x, g x) непрерывна внутри s в x.
LaTeX
$$$\text{ContinuousWithinAt } f s x \to \text{ContinuousWithinAt } g s x \to \text{ContinuousWithinAt } (\lambda x. (f x, g x)) s x$$$
Lean4
@[fun_prop]
theorem snd {f : α → β × γ} {s : Set α} (hf : ContinuousOn f s) : ContinuousOn (fun x => (f x).2) s :=
continuous_snd.comp_continuousOn hf