English
For all a,b,c in a group with isometric left action, nn-distances satisfy nndist(a/b, a/c) = nndist(b,c).
Русский
Для всех a,b,c в группе с изометрическим левым действием выполняется nndist(a/b, a/c) = nndist(b,c).
LaTeX
$$$\operatorname{nndist}(a/b, a/c) = \operatorname{nndist}(b,c)$$$
Lean4
@[to_additive (attr := simp)]
theorem nndist_div_left [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b c : G) :
nndist (a / b) (a / c) = nndist b c := by simp [div_eq_mul_inv]