ratLt_bddAbove — Mathlib

English

For any x ∈ M, the set of rationals strictly below x is bounded above in ℝ.

Русский

Для любого x ∈ M множество рациональных q, удовлетворяющих q < x, ограничено сверху на множестве действительных чисел.

LaTeX

$$$\exists b \in \mathbb{R}, \; \forall q \in \mathbb{Q},\; q < x \Rightarrow q \le b$$$

Lean4

theorem ratLt_bddAbove (x : M) : BddAbove (ratLt x) :=
  by
  obtain ⟨n, hn⟩ := Archimedean.arch x zero_lt_one
  use n
  rw [ratLt, mem_upperBounds]
  intro ⟨num, den, _, _⟩
  rw [Rat.le_iff]
  suffices num • 1 < den • x → num ≤ n * den by simpa using this
  intro h
  exact num_le_nat_mul_den h.le (by simpa using hn)

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