card_Iio

Mathlib.Order.Interval.Finset.Nat

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

English

The set of natural numbers strictly less than b has b elements.

Русский

Множество натуральных чисел, строго меньше b, содержит b элементов.

LaTeX

$$$\forall b \in \mathbb{N},\ |\operatorname{Iio}(b)| = b$$$

Lean4

@[simp]
theorem card_Iio : #(Iio b) = b := by rw [Iio_eq_Ico, card_Ico, Nat.bot_eq_zero, Nat.sub_zero]

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

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

Разделы

Аффилиация

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