uniformContinuous_proj — Mathlib

English

In a product uniform space, the projection onto the i-th coordinate is uniformly continuous.

Русский

В произведении равномерных пространств проекция на i-ю координату равномерно непрерывна.

LaTeX

$$$\\forall i : ι,\\ UniformContinuous (\\lambda a: a_i)$$$

Lean4

theorem uniformContinuous_proj (i : ι) : UniformContinuous fun a : ∀ i : ι, α i => a i :=
  uniformContinuous_pi.1 uniformContinuous_id i

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