im_le_im_mul_exp_dist

Mathlib.Analysis.Complex.UpperHalfPlane.Metric

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.im_le_im_mul_exp_dist

← MathLib Explorer

English

Im(z) ≤ Im(w) · exp(dist(z,w)).

Русский

Im(z) ≤ Im(w) · exp(dist(z,w)).

LaTeX

$$$\\Im(z) \\le \\Im(w) \\cdot e^{\\operatorname{dist}(z,w)}.$$$

Lean4

theorem im_le_im_mul_exp_dist (z w : ℍ) : z.im ≤ w.im * Real.exp (dist z w) :=
  by
  rw [← div_le_iff₀' w.im_pos, ← exp_log z.im_pos, ← exp_log w.im_pos, ← Real.exp_sub, exp_le_exp]
  exact (le_abs_self _).trans (dist_log_im_le z w)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru