real_le_real

Mathlib.Analysis.Complex.Order

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

English

For real x ≤ y, their complex embeddings satisfy (x ≤ y) in ℂ.

Русский

Для действительных x ≤ y их вложение в ℂ сохраняет неравенство.

LaTeX

$$$x \le y \iff (x \le y) \text{ in } \mathbb{C} \text{ after embedding}$$$

Lean4

@[simp, norm_cast]
theorem real_le_real {x y : ℝ} : (x : ℂ) ≤ (y : ℂ) ↔ x ≤ y := by simp [le_def, ofReal]

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

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

Разделы

Аффилиация

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