isClosedEmbedding_coe_rat

Mathlib.Topology.Instances.Rat

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

← MathLib Explorer

English

The natural inclusion ℕ → ℚ is a closed embedding.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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