card_fintypeIco

Mathlib.Order.Interval.Finset.Nat

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

English

The finite cardinality of the half-open interval [a,b) is b−a.

Русский

Конечная кардинальность полузакрытого интервала [a,b) равна b−a.

LaTeX

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

Lean4

@[deprecated Fintype.card_Ico (since := "2025-03-28")]
theorem card_fintypeIco : Fintype.card (Set.Ico a b) = b - a := by simp

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

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

Разделы

Аффилиация

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