isUniformEmbedding_coe_real

Mathlib.Topology.Instances.Rat

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

English

The natural inclusion i: Q → R is a uniform embedding.

Русский

Естественное включение ℚ в ℝ является равномерным вложением.

LaTeX

$$$\\operatorname{IsUniformEmbedding}(\\iota)$$$

Lean4

theorem isUniformEmbedding_coe_real : IsUniformEmbedding ((↑) : ℚ → ℝ) :=
  isUniformEmbedding_comap Rat.cast_injective

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

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

Разделы

Аффилиация

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