English
If f maps s to γ and g maps t to δ with continuity inside their domains, then Prod.map f g is continuous within s×t at (x,y).
Русский
Если f отображает s в γ, а g отображает t в δ, и оба непрерывны внутри своих областей, то Prod.map f g непрерывен внутри s×t в (x,y).
LaTeX
$$$\text{ContinuousWithinAt } f s x \to \text{ContinuousWithinAt } g t y \to \text{ContinuousWithinAt } (Prod.map f g) (s \times\, t) (x, y)$$$
Lean4
theorem prodMap {f : α → γ} {g : β → δ} {s : Set α} {t : Set β} {x : α} {y : β} (hf : ContinuousWithinAt f s x)
(hg : ContinuousWithinAt g t y) : ContinuousWithinAt (Prod.map f g) (s ×ˢ t) (x, y) :=
.prodMk (hf.comp continuousWithinAt_fst mapsTo_fst_prod) (hg.comp continuousWithinAt_snd mapsTo_snd_prod)
