attachFin_Ioo_eq_Ioi

Mathlib.Order.Interval.Finset.Fin

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

English

In Fin(n), the interval Ioo(a,b) equals the interval Ioi(a) when b is the top element.

Русский

В Fin(n) интервал Ioo(a,b) равен интервалу Ioi(a) при верхнем пределе b.

LaTeX

$$$\mathrm{Ioo}(a,b) = \mathrm{Ioi}(a).$$$

Lean4

@[simp]
theorem attachFin_Ioo_eq_Ioi : attachFin (Ioo a n) (fun _x hx ↦ (mem_Ioo.mp hx).2) = Ioi a := by ext; simp

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

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

Разделы

Аффилиация

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