dist_self_mul_right

Mathlib.Analysis.Normed.Group.Uniform

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

English

In a normed group, the distance from a to a b equals the norm of b: dist(a, a b) = ‖b‖.

Русский

В нормированной группе расстояние между a и a b равно норме b: dist(a, a b) = ‖b‖.

LaTeX

$$$\mathrm{dist}(a, a b) = \|b\|.$$$

Lean4

@[to_additive (attr := simp)]
theorem dist_self_mul_right (a b : E) : dist a (a * b) = ‖b‖ := by rw [← dist_one_left, ← dist_mul_left a 1 b, mul_one]

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

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

Разделы

Аффилиация

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