zero_lt_real

Mathlib.Analysis.Complex.Order

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

English

0 < x in ℝ iff 0 < (x : ℂ).

Русский

0 < x в ℝ тогда и только тогда, когда 0 < (x : ℂ).

LaTeX

$$$0 < x \iff 0 < (x : \mathbb{C})$$$

Lean4

@[simp, norm_cast]
theorem zero_lt_real {x : ℝ} : (0 : ℂ) < (x : ℂ) ↔ 0 < x :=
  real_lt_real

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

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

Разделы

Аффилиация

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