card_Ioc_of_le

Mathlib.Data.Int.Interval

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

English

If a ≤ b, then |Ioc(a,b)| = b−a as an integer (cardinality of the half-open interval).

Русский

Если a ≤ b, то |Ioc(a,b)| = b−a как целое число (кардинал полузакрытого интервала).

LaTeX

$$$a \\le b \\Rightarrow \\#(Ioc(a,b)) = b - a$$$

Lean4

theorem card_Ioc_of_le (h : a ≤ b) : (#(Ioc a b) : ℤ) = b - a := by rw [card_Ioc, toNat_sub_of_le h]

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

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

Разделы

Аффилиация

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