dist_fst_le

Mathlib.Analysis.Normed.Lp.ProdLp

URI: https://scilib.ai/kg/mathlib#WithLp.dist_fst_le

English

The distance between the first coordinates is bounded above by the distance of the pairs.

Русский

Расстояние между первыми координатами ограничено сверху расстоянием между парами.

LaTeX

$$$ dist x.fst y.fst \\le dist x y $$$

Lean4

theorem dist_fst_le [PseudoMetricSpace α] [PseudoMetricSpace β] (x y : WithLp p (α × β)) :
    dist x.fst y.fst ≤ dist x y :=
  nndist_fst_le x y

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

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

Разделы

Аффилиация

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