dense_irrational — Mathlib

English

The irrationals are dense in the real line.

Русский

Иррациональные числа плотно лежат в вещественной прямой.

LaTeX

$$$\overline{\{x \in \mathbb{R} \mid \operatorname{Irrational}(x)\}} = \mathbb{R}$$$

Lean4

theorem dense_irrational : Dense {x : ℝ | Irrational x} :=
  by
  refine Real.isTopologicalBasis_Ioo_rat.dense_iff.2 ?_
  simp only [mem_iUnion, mem_singleton_iff, exists_prop, forall_exists_index, and_imp]
  rintro _ a b hlt rfl _
  rw [inter_comm]
  exact exists_irrational_btwn (Rat.cast_lt.2 hlt)

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