denseRange_ratCast — Mathlib

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

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