edist_fst_le

Mathlib.Analysis.Normed.Lp.ProdLp

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

← MathLib Explorer

English

The edistance of the first coordinates is no larger than the edistance of the pair.

Русский

Расстояние по edist для первых координат не превосходит edist самого пары.

LaTeX

$$$ edist x.fst y.fst \\le edist x y $$$

Lean4

theorem edist_fst_le [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x y : WithLp p (α × β)) :
    edist x.fst y.fst ≤ edist x y :=
  (edist_proj_le_edist_aux p x y).1

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

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

Разделы

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

Аффилиация

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