card_fintypeIio

Mathlib.Order.Interval.Finset.Fin

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

English

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

Русский

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

LaTeX

$$|Iio(b)| = b$$

Lean4

@[deprecated Fintype.card_Iio (since := "2025-03-28")]
theorem card_fintypeIio : Fintype.card (Set.Iio b) = b := by simp

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

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

Разделы

Аффилиация

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