English
The intersection of all initial segments (-∞, q] with q ∈ ℚ is empty: there is no real number that is ≤ every rational q.
Русский
Пересечение всех начальных участков (-∞, q] по всем q ∈ ℚ равно пустому множеству: не существует вещественного x, который был бы меньше или равен каждому рациональному q.
LaTeX
$$$$\bigcap_{q\in \mathbb{Q}}(-\infty, q] = \varnothing.$$$$
Lean4
theorem iInter_Iic_rat : ⋂ r : ℚ, Iic (r : ℝ) = ∅ := by exact iInter_Iic_eq_empty_iff.mpr not_bddBelow_coe