zero_le_real

Mathlib.Analysis.Complex.Order

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp, norm_cast]
theorem zero_le_real {x : ℝ} : (0 : ℂ) ≤ (x : ℂ) ↔ 0 ≤ x :=
  real_le_real

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

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

Разделы

Аффилиация

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