card_Icc

Mathlib.Order.Interval.Finset.Nat

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

English

The number of elements in the closed interval [a,b] is b+1−a.

Русский

Количество элементов в замкнутом интервале [a,b] равно b+1−a.

LaTeX

$$$\forall a,b \in \mathbb{N},\ |\operatorname{Icc}(a,b)| = b + 1 - a$$$

Lean4

@[simp]
theorem card_Icc : #(Icc a b) = b + 1 - a :=
  List.length_range' ..

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

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

Разделы

Аффилиация

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