dist_div_left — Mathlib

English

For all a,b,c in a group G with a metric, dist(a/b, a/c) = dist(b,c).

Русский

Для любых a,b,c в группе G с заданной метрикой выполняется d(a/b, a/c) = d(b,c).

LaTeX

$$$\operatorname{dist}(a/b, a/c) = \operatorname{dist}(b,c)$$$

Lean4

@[to_additive (attr := simp)]
theorem dist_div_left [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b c : G) :
    dist (a / b) (a / c) = dist b c := by simp [div_eq_mul_inv]

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