card_fintypeIic

Mathlib.Order.Interval.Finset.Nat

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

English

The finite cardinality of the left-closed interval [−∞,b] in Nat is b+1.

Русский

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

LaTeX

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

Lean4

@[deprecated Fintype.card_Iic (since := "2025-03-28")]
theorem card_fintypeIic : Fintype.card (Set.Iic b) = b + 1 := by simp

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

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

Разделы

Аффилиация

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