card_fintypeIoo

Mathlib.Order.Interval.Finset.Nat

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

English

The finite cardinality of the interval (a,b) is b−a−1.

Русский

Конечная кардинальность интервала (a,b) равна b−a−1.

LaTeX

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

Lean4

@[deprecated Fintype.card_Ioo (since := "2025-03-28")]
theorem card_fintypeIoo : Fintype.card (Set.Ioo a b) = b - a - 1 := by simp

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

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

Разделы

Аффилиация

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