prodMk_right

Mathlib.Topology.EMetricSpace.Lipschitz

URI: https://scilib.ai/kg/mathlib#LocallyLipschitz.prodMk_right

English

The map a ↦ (a, b) is locally Lipschitz for fixed b.

Русский

Карта a ↦ (a, b) локально липшицева для фиксированного b.

LaTeX

$$$\\forall b,\\ LocallyLipschitz(\\lambda a. (a,b))$$$

Lean4

protected theorem prodMk_right (b : β) : LocallyLipschitz (fun a : α => (a, b)) :=
  (LipschitzWith.prodMk_right b).locallyLipschitz

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

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

Разделы

Аффилиация

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