prod_lipschitzWith_ofLp — Mathlib

English

The map ofLp p : (α × β) → WithLp p (α × β) is 1-Lipschitz.

Русский

Карта $\\mathrm{ofLp}_p\$ с произвольным произведением является 1-Липшицевой.

LaTeX

$$$ \\text{LipschitzWith}_1\\bigl( \\operatorname{ofLp}_p : (\\alpha \\times \\beta) \\to \\mathrm{WithLp}_p(\\alpha \\times \\beta) \\bigr) $$$

Lean4

theorem prod_lipschitzWith_ofLp [PseudoEMetricSpace α] [PseudoEMetricSpace β] : LipschitzWith 1 (@ofLp p (α × β)) :=
  prod_lipschitzWith_ofLp_aux p α β

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