equivRealProd_apply_le

Mathlib.Analysis.Complex.Basic

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

English

For z ∈ ℂ, the norm of equivRealProd(z) is bounded above by the norm of z: ‖equivRealProd z‖ ≤ ‖z‖.

Русский

Для z ∈ ℂ нормa equivRealProd(z) не выше нормы z: \\|equivRealProd z\\| ≤ \\|z\\|.

LaTeX

$$$ \\|equivRealProd(z)\\| \\leq \\|z\\| $$$

Lean4

theorem equivRealProd_apply_le (z : ℂ) : ‖equivRealProd z‖ ≤ ‖z‖ := by
  simp [Prod.norm_def, abs_re_le_norm, abs_im_le_norm]

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

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

Разделы

Аффилиация

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