ofReal_le_ofReal

Mathlib.Analysis.RCLike.Basic

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

English

For all real x, y, the embedding preserves order: (x : K) ≤ (y : K) is equivalent to x ≤ y.

Русский

Для любых вещественных x, y вложение сохраняет порядок: (x : K) ≤ (y : K) эквивалентно x ≤ y.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem ofReal_le_ofReal {x y : ℝ} : (x : K) ≤ (y : K) ↔ x ≤ y :=
  by
  rw [le_iff_re_im]
  simp

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

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

Разделы

Аффилиация

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