eval — Mathlib

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

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