English
The evaluation map at i is 1-Lipschitz: LipschitzWith 1 (Function.eval i).
Русский
Проекция на координату i в произведении функций является 1‑липшицевой: LipschitzWith 1 (Function.eval i).
LaTeX
$$$\\operatorname{LipschitzWith} 1 (\\operatorname{Function.eval} i)$$$
Lean4
protected theorem eval {α : ι → Type u} [∀ i, PseudoEMetricSpace (α i)] [Fintype ι] (i : ι) :
LipschitzWith 1 (Function.eval i : (∀ i, α i) → α i) :=
LipschitzWith.of_edist_le fun f g => by convert edist_le_pi_edist f g i