card_Iic

Mathlib.Order.Interval.Finset.Nat

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

English

The set of natural numbers less than or equal to b has b+1 elements.

Русский

Множество натуральных чисел, не превосходящих b, содержит b+1 элементов.

LaTeX

$$$\forall b \in \mathbb{N},\ |\operatorname{Iic}(b)| = b + 1$$$

Lean4

@[simp]
theorem card_Iic : #(Iic b) = b + 1 := by rw [Iic_eq_Icc, card_Icc, Nat.bot_eq_zero, Nat.sub_zero]

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

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

Разделы

Аффилиация

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