iUnion_Iic_rat — Mathlib

English

Every real number lies below some rational number; equivalently, the union of all initial segments (-∞, q] for q ∈ ℚ equals the entire real line.

Русский

Каждое вещественное число лежит не выше некоторого рационального; эквивалентно тому, что объединение всех предельных сегментов (-∞, q] для q ∈ ℚ равно всей ℝ.

LaTeX

$$$$\bigcup_{q\in \mathbb{Q}}(-\infty, q] = \mathbb{R}.$$$$

Lean4

theorem iUnion_Iic_rat : ⋃ r : ℚ, Iic (r : ℝ) = univ := by exact iUnion_Iic_of_not_bddAbove_range not_bddAbove_coe

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