abs_re_div_norm_le_one

Mathlib.Analysis.Complex.Norm

URI: https://scilib.ai/kg/mathlib#Complex.abs_re_div_norm_le_one

← MathLib Explorer

English

For all z, |Re z / ||z||| ≤ 1 (with the trivial case z = 0 giving 0 ≤ 1).

Русский

Для любого z: |Re z / ||z||| ≤ 1 (случай z = 0 тривиален).

LaTeX

$$$$\\left| \\frac{\\Re z}{ \\|z\\|} \\right| \\le 1$$$$

Lean4

theorem abs_re_div_norm_le_one (z : ℂ) : |z.re / ‖z‖| ≤ 1 :=
  if hz : z = 0 then by simp [hz, zero_le_one]
  else by simp_rw [abs_div, abs_norm, div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_re_le_norm]

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

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

Разделы

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

Аффилиация

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