not_bddBelow_coe — Mathlib

English

The rationals considered as a subset of the real numbers are not bounded below: for every real L there exists a rational q with q < L.

Русский

Рациональные числа, как множество в ℝ, не ограничены снизу: для любого вещественного числа L существует рациональное q, такое что q < L.

LaTeX

$$$\\forall L \\in \\mathbb{R},\\exists q \\in \\mathbb{Q}, q < L.$$$

Lean4

theorem not_bddBelow_coe : ¬(BddBelow <| range (fun (x : ℚ) ↦ (x : ℝ))) :=
  by
  dsimp only [BddBelow, lowerBounds]
  rw [Set.not_nonempty_iff_eq_empty]
  ext
  simpa using exists_rat_lt _

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