Ici_eq_finset_subtype

Mathlib.Order.Interval.Finset.Fin

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

English

Ici(a) in Fin(n) equals fin(n) of Ico(a.val,n).

Русский

Ici(a) в Fin(n) равен fin(n) от Ico(a.val,n).

LaTeX

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

Lean4

@[deprecated attachFin_Ico_eq_Ici (since := "2025-04-06")]
theorem Ici_eq_finset_subtype : Ici a = (Ico (a : ℕ) n).fin n := by ext; simp

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

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

Разделы

Аффилиация

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