isUniformEmbedding_coe_rat

Mathlib.Topology.Instances.Rat

URI: https://scilib.ai/kg/mathlib#Int.isUniformEmbedding_coe_rat

← MathLib Explorer

English

The inclusion ℤ → ℚ is a uniform embedding.

Русский

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

LaTeX

$$$\\operatorname{IsUniformEmbedding}(\\iota: \\mathbb{Z} \\to \\mathbb{Q})$$$

Lean4

theorem isUniformEmbedding_coe_rat : IsUniformEmbedding ((↑) : ℤ → ℚ) :=
  isUniformEmbedding_bot_of_pairwise_le_dist zero_lt_one <| by simpa using Int.pairwise_one_le_dist

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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