isUniformEmbedding_coe

Mathlib.Topology.Instances.PNat

URI: https://scilib.ai/kg/mathlib#PNat.isUniformEmbedding_coe

English

The inclusion ℕ+ → ℕ is a uniform embedding.

Русский

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

LaTeX

$$$\operatorname{IsUniformEmbedding}(\operatorname{Subtype.val})$$$

Lean4

theorem isUniformEmbedding_coe : IsUniformEmbedding ((↑) : ℕ+ → ℕ) :=
  isUniformEmbedding_subtype_val

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

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

Разделы

Аффилиация

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