natEmbedding

Mathlib.Data.Set.Finite.Basic

URI: https://scilib.ai/kg/mathlib#Set.Infinite.natEmbedding

English

Embedding of ℕ into an infinite subset s of α.

Русский

Встраивание \mathbb{N} в бесконечную подмножество s ⊆ α.

LaTeX

$$$ \exists i: \mathbb{N} \hookrightarrow s \quad \text{if } s \text{ Infinite}$$$

Lean4

/-- Embedding of `ℕ` into an infinite set. -/
noncomputable def natEmbedding (s : Set α) (h : s.Infinite) : ℕ ↪ s :=
  h.to_subtype.natEmbedding

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

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

Разделы

Аффилиация

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