continuousOn_pi' — Mathlib

English

If for every i the restriction of f to i-th coordinate is ContinuousOn on s, then f is ContinuousOn on s.

Русский

Если для каждого i ограничение f к i-й координате непрерывно на s, то сама функция f непрерывна на s.

LaTeX

$$$$\bigl(\forall i,\text{ ContinuousOn }(\lambda y. f(y)(i))\ s\bigr) \Rightarrow \text{ ContinuousOn } f\ s.$$$$

Lean4

@[fun_prop]
theorem continuousOn_pi' {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] {f : α → ∀ i, X i} {s : Set α}
    (hf : ∀ i, ContinuousOn (fun y => f y i) s) : ContinuousOn f s :=
  continuousOn_pi.2 hf

Похожие утверждения