card_Ioo_of_lt

Mathlib.Data.Int.Interval

URI: https://scilib.ai/kg/mathlib#Int.card_Ioo_of_lt

English

If a < b, then |Ioo(a,b)| = b−a−1 as an integer (cardinality of the open interval).

Русский

Если a < b, то |Ioo(a,b)| = b−a−1 как целое число (кардинал открытого интервала).

LaTeX

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

Lean4

theorem card_Ioo_of_lt (h : a < b) : (#(Ioo a b) : ℤ) = b - a - 1 := by rw [card_Ioo, sub_sub, toNat_sub_of_le h]

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

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

Разделы

Аффилиация

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