prod_snd

Mathlib.Topology.EMetricSpace.Lipschitz

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

English

The projection onto the second factor is 1-Lipschitz.

Русский

Проекция на вторую координату является 1‑липшицевой.

LaTeX

$$$\\text{LipschitzWith } 1 \\; \\mathrm{Prod.snd}$$$

Lean4

protected theorem prod_snd : LipschitzWith 1 (@Prod.snd α β) :=
  LipschitzWith.of_edist_le fun _ _ => le_max_right _ _

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

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

Разделы

Аффилиация

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