lipschitzWith_ofLp

Mathlib.Analysis.Normed.Lp.PiLp

URI: https://scilib.ai/kg/mathlib#PiLp.lipschitzWith_ofLp

English

The map toLp is Lipschitz with a constant depending on the index cardinality.

Русский

Карта кtoLp является липшицевой с константой, зависящей от числа индексов.

LaTeX

$$LipschitzWith 1 (WithLp.ofLp p)$$

Lean4

theorem lipschitzWith_ofLp [∀ i, PseudoEMetricSpace (β i)] : LipschitzWith 1 (@ofLp p (∀ i, β i)) :=
  lipschitzWith_ofLp_aux p β

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru