uniformContinuous_vadd — Mathlib

English

The addition map (v,p) ↦ v +ᵥ p is uniformly continuous from V × P to P.

Русский

Отображение (v,p) ↦ v +ᵥ p с единым модулем непрерывности из V × P в P равномерно непрерывно.

LaTeX

$$$\operatorname{UniformContinuous}\big((v,p) \mapsto v +ᵥ p\big)$$$

Lean4

theorem uniformContinuous_vadd : UniformContinuous fun x : V × P => x.1 +ᵥ x.2 :=
  (LipschitzWith.prod_fst.vadd LipschitzWith.prod_snd).uniformContinuous

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