continuousOn_apply — Mathlib

English

If X i are spaces and i indexes, the map p ↦ p i from the product to X i is ContinuousOn for any fixed i.

Русский

Для фиксированного i отображение p ↦ p(i) из произведения в X_i непрерывно на s.

LaTeX

$$$$\text{ContinuousOn}(p \mapsto p(i))\ s.$$$$

Lean4

@[fun_prop]
theorem continuousOn_apply {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] (i : ι) (s) :
    ContinuousOn (fun p : ∀ i, X i => p i) s :=
  Continuous.continuousOn (continuous_apply i)

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