attachFin_Ico_eq_Ici

Mathlib.Order.Interval.Finset.Fin

URI: https://scilib.ai/kg/mathlib#Fin.attachFin_Ico_eq_Ici

English

In Fin(n), the half-open interval Ico(a,n) coincides with the closed interval Ici(a).

Русский

В Fin(n) полуоткрытый интервал Ico(a,n) совпадает с закрытым интервалом Ici(a).

LaTeX

$$$\mathrm{Ico}(a,n) = \mathrm{Ici}(a).$$$

Lean4

@[simp]
theorem attachFin_Ico_eq_Ici : attachFin (Ico a n) (fun _x hx ↦ (mem_Ico.mp hx).2) = Ici a := by ext; simp

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

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

Разделы

Аффилиация

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