dist_inv — Mathlib

English

In a seminormed group, the distance is invariant under inversion on either side: dist(x⁻¹, y) = dist(x, y⁻¹).

Русский

В полугруппе с нормой расстояние сохраняется при взятии обратной слева или справа: dist(x⁻¹, y) = dist(x, y⁻¹).

LaTeX

$$$$\operatorname{dist}(x^{-1}, y) = \operatorname{dist}(x, y^{-1}).$$$$

Lean4

@[to_additive]
theorem dist_inv (x y : E) : dist x⁻¹ y = dist x y⁻¹ := by
  simp_rw [dist_eq_norm_div, ← norm_inv' (x⁻¹ / y), inv_div, div_inv_eq_mul, mul_comm]

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