card_fintypeIic

Mathlib.Order.Interval.Finset.Fin

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

English

For any b ∈ Fin n, the cardinality of the set { x ∈ Fin n : x ≤ b } equals b + 1.

Русский

Для любого b ∈ Fin n число элементов { x ∈ Fin n : x ≤ b } равно b + 1.

LaTeX

$$|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