nats

Mathlib.Data.Stream.Defs

URI: https://scilib.ai/kg/mathlib#Stream'.nats

English

The stream of natural numbers: nats(n) = n.

Русский

Поток натуральных чисел: nats(n) = n.

LaTeX

$$$ \forall n \in \mathbb{N},\ nats(n) = n. $$$

Lean4

/-- The stream of natural numbers: `Stream'.get n Stream'.nats = n`. -/
def nats : Stream' ℕ := fun n => n

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

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

Разделы

Аффилиация

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