card_Ioo

Mathlib.Data.PNat.Interval

URI: https://scilib.ai/kg/mathlib#PNat.card_Ioo

English

For a,b ∈ ℕ+, the number of PNats in the open interval Ioo a b equals b − a − 1.

Русский

Для a,b ∈ ℕ+ число PNats в открытом интервале Ioo a b равно b − a − 1.

LaTeX

$$$\\#(Ioo(a,b)) = b - a - 1$$$

Lean4

@[simp]
theorem card_Ioo : #(Ioo a b) = b - a - 1 := by rw [← Nat.card_Ioo, ← map_subtype_embedding_Ioo, card_map]

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

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

Разделы

Аффилиация

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