dist_eq_iff_eq_sq_sinh — Mathlib

English

If r ≥ 0, then dist(z,w) = r is equivalent to dist(z,w)^2/(4 z.im w.im) = sinh(r/2)^2.

Русский

Если r ≥ 0, то dist(z,w) = r эквивалентно [dist(z,w)]^2/(4 z.im w.im) = sinh(r/2)^2.

LaTeX

$$$dist(z,w) = r \iff dist(z,w)^2 /(4 \cdot z.im \cdot w.im) = \sinh(r/2)^2$$$

Lean4

theorem dist_eq_iff_eq_sq_sinh (hr : 0 ≤ r) :
    dist z w = r ↔ dist (z : ℂ) w ^ 2 / (4 * z.im * w.im) = sinh (r / 2) ^ 2 :=
  by
  rw [dist_eq_iff_eq_sinh, ← sq_eq_sq₀, div_pow, mul_pow, sq_sqrt, mul_assoc]
  · norm_num
  all_goals positivity

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