card_fintypeIcc

Mathlib.Order.Interval.Finset.Nat

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

English

The finite cardinality of the closed interval [a,b] is b+1−a.

Русский

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

LaTeX

$$$\forall a,b \in \mathbb{N},\ \mathrm{Fintype.card}(\mathrm{Set.Icc}(a,b)) = b + 1 - a$$$

Lean4

@[deprecated Fintype.card_Icc (since := "2025-03-28")]
theorem card_fintypeIcc : Fintype.card (Set.Icc a b) = b + 1 - a := by simp

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

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

Разделы

Аффилиация

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