dist_inv_inv₀ — Mathlib

English

For nonzero z,w, the distance between their inverses satisfies: dist(z^{-1}, w^{-1}) = dist(z, w) / (|z| |w|).

Русский

Пусть z,w ≠ 0; расстояние между их обратными принадлежностями: dist(z^{-1}, w^{-1}) = dist(z, w) / (|z| |w|).

LaTeX

$$$\operatorname{dist}(z^{-1}, w^{-1}) = \dfrac{\operatorname{dist}(z, w)}{\|z\| \|w\|}$$$

Lean4

theorem dist_inv_inv₀ {z w : α} (hz : z ≠ 0) (hw : w ≠ 0) : dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖) := by
  rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹, mul_assoc,
    dist_eq_norm', div_eq_mul_inv, mul_inv]

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