range_succ

Mathlib.Data.Multiset.Range

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

← MathLib Explorer

English

range (succ n) equals n added to range n.

Русский

range (succ n) = n :: range n (мультимножество).

LaTeX

$$$\mathrm{range}(\mathrm{succ}(n)) = n ::\_{m} \mathrm{range}(n)$$$

Lean4

@[simp]
theorem range_succ (n : ℕ) : range (succ n) = n ::ₘ range n := by
  rw [range, List.range_succ, ← coe_add, Multiset.add_comm, range, coe_singleton, singleton_add]

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

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

Разделы

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

Аффилиация

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