nndist_div_left — Mathlib

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]

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