isClosedEmbedding_coe_rat

Mathlib.Topology.Instances.Rat

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

← MathLib Explorer

English

The inclusion ℤ → ℚ is a closed embedding.

Русский

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

LaTeX

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

Lean4

theorem isClosedEmbedding_coe_rat : IsClosedEmbedding ((↑) : ℤ → ℚ) :=
  isClosedEmbedding_of_pairwise_le_dist zero_lt_one <| by simpa using Int.pairwise_one_le_dist

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

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

Разделы

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

Аффилиация

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