prodMk_left

Mathlib.Topology.EMetricSpace.Lipschitz

URI: https://scilib.ai/kg/mathlib#LipschitzWith.prodMk_left

← MathLib Explorer

English

For any a, the map b ↦ (a, b) is 1-Lipschitz.

Русский

Для любого a отображение b ↦ (a, b) является 1‑липшицевым.

LaTeX

$$$\\text{LipschitzWith } 1 (\\mathrm{Prod.mk}\\ a : β \\to α \\times β)$$$

Lean4

protected theorem prodMk_left (a : α) : LipschitzWith 1 (Prod.mk a : β → α × β) := by
  simpa only [max_eq_right zero_le_one] using (LipschitzWith.const a).prodMk LipschitzWith.id

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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