attachFin_Iic

Mathlib.Order.Interval.Finset.Fin

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

English

In Fin(n), the Iic interval equals the corresponding finite-embedding of Iic(a.val).

Русский

В Fin(n) интервал Iic совпадает с соответствующим образом вложенным Iic(a.val).

LaTeX

$$$\mathrm{Iic}(a) = \mathrm{fin}(n)(\mathrm{Iic}(a.val)).$$$

Lean4

@[simp]
theorem attachFin_Iic : attachFin (Iic a) (fun _x hx ↦ (mem_Iic.mp hx).trans_lt a.2) = Iic a := by ext; simp

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

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

Разделы

Аффилиация

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