ratLt_nonempty — Mathlib

English

There exists a rational number strictly less than x.

Русский

Существует рациональная величина, строго меньшая x.

LaTeX

$$$\exists q \in \mathbb{Q},\; q < x$$$

Lean4

theorem ratLt_nonempty (x : M) : (ratLt x).Nonempty :=
  by
  obtain hneg | rfl | hxpos := lt_trichotomy x 0
  · obtain ⟨n, hn⟩ := Archimedean.arch (-x - x) zero_lt_one
    use Rat.ofInt (-n)
    suffices -(n • 1) < x by simpa using this
    exact neg_lt.mpr (lt_of_lt_of_le (by simpa using hneg) hn)
  · exact ⟨Rat.ofInt (-1), by simp⟩
  · obtain ⟨n, hn⟩ := Archimedean.arch 1 hxpos
    use Rat.mk' 1 (n + 1) (by simp) (by simp)
    simpa using hn.trans_lt <| (nsmul_lt_nsmul_iff_left hxpos).mpr (by simp)

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