card_fintype_Ioc_of_le

Mathlib.Data.Int.Interval

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

English

If a ≤ b, then (Fintype.card (Set.Ioc a b)) as an integer equals b−a.

Русский

Если a ≤ b, то (Fintype.card(Set.Ioc a b)) как целое число равно b−a.

LaTeX

$$$a \\le b \\Rightarrow (\\mathrm{Fintype.card}(\\mathrm{Set.Ioc}(a,b)) : \\mathbb{Z}) = b - a$$$

Lean4

theorem card_fintype_Ioc_of_le (h : a ≤ b) : (Fintype.card (Set.Ioc a b) : ℤ) = b - a := by simp [h]

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

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

Разделы

Аффилиация

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