abs_arg_le_pi_div_two_iff

Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

← MathLib Explorer

English

For z ∈ ℂ, |arg z| ≤ π/2 if and only if Re z ≥ 0.

Русский

Для z ∈ ℂ, |arg z| ≤ π/2 тогда и только тогда, когда Re z ≥ 0.

LaTeX

$$$|\\\\arg z| \\\\le \\\\frac{\\\\pi}{2} \\\\iff 0 \\\\le \\\\Re z$$$

Lean4

@[simp]
theorem abs_arg_le_pi_div_two_iff {z : ℂ} : |arg z| ≤ π / 2 ↔ 0 ≤ re z := by
  rw [abs_le, arg_le_pi_div_two_iff, neg_pi_div_two_le_arg_iff, ← or_and_left, ← not_le, and_not_self_iff, or_false]

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

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

Разделы

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

Аффилиация

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