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