not_bddAbove_coe — Mathlib

English

The rationals contained in the real line are not bounded above: for every real number M there exists a rational q with q > M.

Русский

Рациональные числа, рассмотренные как подмножество действительных чисел, не ограничены сверху: для любого вещественного числа M существует рациональное q such that q > M.

LaTeX

$$$\\neg\\operatorname{BddAbove}\\left\$\\operatorname{range}(\\lambda x: x \\in\\mathbb{Q} \\mapsto x)\\right\$.$$

Lean4

theorem not_bddAbove_coe : ¬(BddAbove <| range (fun (x : ℚ) ↦ (x : ℝ))) :=
  by
  dsimp only [BddAbove, upperBounds]
  rw [Set.not_nonempty_iff_eq_empty]
  ext
  simpa using exists_rat_gt _

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