re_nonneg_of_nonneg

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.re_nonneg_of_nonneg

English

If x is self-adjoint, then 0 ≤ Re(x) iff 0 ≤ x.

Русский

Если x самосопряжено, то 0 ≤ Re(x) эквивалентно 0 ≤ x.

LaTeX

$$$ \text{IsSelfAdjoint}(x) \Rightarrow \bigl( 0 \le \operatorname{re}(x) \iff 0 \le x \bigr) $$$

Lean4

theorem re_nonneg_of_nonneg {x : K} (hx : IsSelfAdjoint x) : 0 ≤ re x ↔ 0 ≤ x := by
  simp [nonneg_iff (K := K), conj_eq_iff_im.mp hx]

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

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

Разделы

Аффилиация

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