lt_def

Mathlib.Analysis.Complex.Order

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

English

Let z,w ∈ ℂ. Then z < w if and only if the real parts satisfy Re(z) < Re(w) and the imaginary parts are equal: Im(z) = Im(w).

Русский

Пусть z,w ∈ ℂ. Тогда z < w по порядку ℂ эквивалентно Re(z) < Re(w) и Im(z) = Im(w).

LaTeX

$$$$ z < w \iff \Re(z) < \Re(w) \land \Im(z) = \Im(w) $$$$

Lean4

theorem lt_def {z w : ℂ} : z < w ↔ z.re < w.re ∧ z.im = w.im :=
  Iff.rfl

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

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

Разделы

Аффилиация

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