isDenseEmbedding_coe_real

Mathlib.Topology.Instances.Rat

URI: https://scilib.ai/kg/mathlib#Rat.isDenseEmbedding_coe_real

English

The inclusion i: ℚ → ℝ has dense range; i(ℚ) is dense in ℝ.

Русский

Образ ℚ во множества ℝ плотен; i(ℚ) плотно в ℝ.

LaTeX

$$$\\overline{\\iota(\\mathbb{Q})} = \\mathbb{R}$$$

Lean4

theorem isDenseEmbedding_coe_real : IsDenseEmbedding ((↑) : ℚ → ℝ) :=
  isUniformEmbedding_coe_real.isDenseEmbedding Rat.denseRange_cast

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru