edist_snd_le

Mathlib.Analysis.Normed.Lp.ProdLp

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$ edist x.snd y.snd \\le edist x y $$$

Lean4

theorem edist_snd_le [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x y : WithLp p (α × β)) :
    edist x.snd y.snd ≤ edist x y :=
  (edist_proj_le_edist_aux p x y).2

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

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

Разделы

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

Аффилиация

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