dist_le_dist_coe_div_sqrt — Mathlib

English

The distance in the upper half-plane is bounded by the Euclidean distance between the complex embeddings divided by the square root of the product of imaginary parts.

Русский

Расстояние в верхней полуплоскости ограничено евклидовским расстоянием между соответствующими комплексными образами, делённым на квадратный корень из произведения мнимых частей.

LaTeX

$$$dist(z,w) ≤ dist(z,\; w)_{\mathbb{C}} / \sqrt{z.im \cdot w.im}$$$

Lean4

theorem dist_le_dist_coe_div_sqrt (z w : ℍ) : dist z w ≤ dist (z : ℂ) w / √(z.im * w.im) :=
  by
  rw [dist_le_iff_le_sinh, ← div_mul_eq_div_div_swap, self_le_sinh_iff]
  positivity

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