ratCast_lt — Mathlib

English

For all x,y ∈ ℚ, the order is preserved by the real embedding: x < y in ℚ iff x (as a real) < y (as a real).

Русский

Для всех x,y ∈ ℚ порядок сохраняется при отображении в ℝ: x < y в ℚ эквивалентно x < y как вещественные.

LaTeX

$$$\forall x,y:\mathbb{Q},\ (x< y)_{\mathbb{R}} \iff x< y$$$

Lean4

theorem ratCast_lt {x y : ℚ} : (x : ℝ) < (y : ℝ) ↔ x < y :=
  by
  rw [← mk_const, ← mk_const, mk_lt]
  exact const_lt

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