Icc_eq_range'

Mathlib.Order.Interval.Finset.Nat

URI: https://scilib.ai/kg/mathlib#Nat.Icc_eq_range'

English

In natural numbers, the closed interval Icc(a,b) consists exactly of the consecutive integers a, a+1, ..., b.

Русский

В натуральных числах замкнутый интервал Icc(a,b) состоит ровно из последовательных целых чисел a, a+1, ..., b.

LaTeX

$$Icc(a,b) = { a, a+1, \dots, b }$$

Lean4

theorem Icc_eq_range' : Icc a b = ⟨List.range' a (b + 1 - a), List.nodup_range'⟩ :=
  rfl

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

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

Разделы

Аффилиация

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