English
Let φ: ℚ → EReal be the natural embedding r ↦ (r : ℝ) viewed in EReal. Then the image φ(ℚ) is dense in EReal.
Русский
Пусть φ: ℚ → EReal обозначает естественное вложение, r ↦ (r : ℝ) в EReal. Тогда образ φ(ℚ) плотно лежит в EReal.
LaTeX
$$$\\operatorname{DenseRange}\\left( \\lambda r:\\mathbb{Q}, (r:\\mathbb{R}):\\mathrm{EReal} \\right)$$$
Lean4
theorem denseRange_ratCast : DenseRange (fun r : ℚ ↦ ((r : ℝ) : EReal)) :=
dense_of_exists_between fun _ _ h => exists_range_iff.2 <| exists_rat_btwn_of_lt h