edist_congr

Mathlib.Topology.EMetricSpace.Defs

URI: https://scilib.ai/kg/mathlib#edist_congr

← MathLib Explorer

English

If edist w x = 0 and edist y z = 0, then edist w y = edist x z.

Русский

Если edist w x = 0 и edist y z = 0, то edist w y = edist x z.

LaTeX

$$$ edist\ w\ x = 0 \land edist\ y\ z = 0 \Rightarrow edist\ w\ y = edist\ x\ z $$$

Lean4

theorem edist_congr {w x y z : α} (hl : edist w x = 0) (hr : edist y z = 0) : edist w y = edist x z :=
  (edist_congr_right hl).trans (edist_congr_left hr)

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

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

Разделы

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

Аффилиация

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