card_fintypeIio

Mathlib.Order.Interval.Finset.Nat

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

English

The finite cardinality of the strictly left interval {x ∈ Nat | x < b} is b.

Русский

Конечная кардинальность множества {x ∈ Nat | x < b} равна b.

LaTeX

$$$\forall b \in \mathbb{N},\ \mathrm{Fintype.card}(\mathrm{Set.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