ofReal_lt_ofReal

Mathlib.Analysis.RCLike.Basic

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

English

The embedding preserves strict order: (x : K) < (y : K) if and only if x < y for real x, y.

Русский

Вложение сохраняет строгий порядок: (x : K) < (y : K) тогда и только тогда, когда x < y для вещественных x, y.

LaTeX

$$$ (x : K) < (y : K) \iff x < y $$$

Lean4

@[simp, norm_cast]
theorem ofReal_lt_ofReal {x y : ℝ} : (x : K) < (y : K) ↔ x < y :=
  by
  rw [lt_iff_re_im]
  simp

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

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

Разделы

Аффилиация

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