prod_fst

Mathlib.Topology.EMetricSpace.Lipschitz

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

English

The projection onto the first factor is 1-Lipschitz.

Русский

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

LaTeX

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

Lean4

protected theorem prod_fst : LipschitzWith 1 (@Prod.fst α β) :=
  LipschitzWith.of_edist_le fun _ _ => le_max_left _ _

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

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

Разделы

Аффилиация

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