English
For a family X i of topological spaces indexed by ι, a function f: α → ∀ i, X i is ContinuousWithinAt on s at x if and only if for every i, the function y ↦ f(y)(i) is ContinuousWithinAt on s at x.
Русский
Для семейства пространств X_i индексируемого множества ι, функция f: α → ∀ i, X_i непрерывна на s в x тогда и только тогда, когда для каждого i функция y ↦ f(y)(i) непрерывна на s в x.
LaTeX
$$$$\text{ContinuousWithinAt } f\ s\ x \iff \forall i, \ \text{ContinuousWithinAt }(\lambda y. f(y)(i))\ s\ x.$$$$
Lean4
theorem continuousWithinAt_pi {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] {f : α → ∀ i, X i} {s : Set α}
{x : α} : ContinuousWithinAt f s x ↔ ∀ i, ContinuousWithinAt (fun y => f y i) s x :=
tendsto_pi_nhds
