continuousAt_apply — Mathlib

English

For any index i, the projection map from the product space ∀ i, A_i to A_i, given by p ↦ p(i), is continuous at every point x, i.e., the ith coordinate projection is continuous.

Русский

Пусть i — индекс, тогда проекция из произведения ∏_i A_i на i-ю координату, p ↦ p(i), непрерывна во всякой точке x.

LaTeX

$$$ContinuousAt(\\lambda p: \\prod_{i} A_i, p(i))\\; x$$$

Lean4

theorem continuousAt_apply (i : ι) (x : ∀ i, A i) : ContinuousAt (fun p : ∀ i, A i => p i) x :=
  (continuous_apply i).continuousAt

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