re_neg_ne_zero_of_re_pos

Mathlib.Analysis.Complex.Norm

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

English

If the real part of s is positive, then the real part of −s is nonzero.

Русский

Если вещественная часть числа s положительна, то вещественная часть −s не нулевая.

LaTeX

$$$\\Re(s) > 0 \\implies (\\Re(-s) \\\\neq 0)$$$

Lean4

theorem re_neg_ne_zero_of_re_pos {s : ℂ} (hs : 0 < s.re) : (-s).re ≠ 0 :=
  ne_iff_lt_or_gt.mpr <| Or.inl <| neg_re s ▸ (neg_lt_zero.mpr hs)

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

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

Разделы

Аффилиация

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