dist_ofAdd

Mathlib.Topology.MetricSpace.Defs

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

English

The distance is preserved under the identification of elements through the Mul operation.

Русский

Расстояние сохраняется при идентификации элементов через операцию mul.

LaTeX

$$dist\; (ofMul\; a)\; (ofMul\; b) = dist\; a\; b$$

Lean4

@[simp]
theorem dist_ofAdd (a b : X) : dist (ofAdd a) (ofAdd b) = dist a b :=
  rfl

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

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

Разделы

Аффилиация

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