range_succ

Mathlib.Data.Nat.Set

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

English

The range of the successor function on natural numbers is the set of positive integers.

Русский

Диапазон функции successors на натуральных числах есть множество положительных целых чисел.

LaTeX

$$$ \\mathrm{range}(\\mathrm{succ}) = \\{ i \\in \\mathbb{N} \\mid 0 < i \\}$$$

Lean4

@[simp]
protected theorem range_succ : range succ = {i | 0 < i} := by ext (_ | i) <;> simp

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

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

Разделы

Аффилиация

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