iInter_Iic_rat — Mathlib

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

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