finsetImage_val_Ici

Mathlib.Order.Interval.Finset.Fin

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

English

The Nat-valued image of the Ici interval equals the Nat Ico interval starting at a.val and ending at n.

Русский

Изображение в ℕ интервалы Ici(a) даёт Nat-интервал Ico(a.val, n).

LaTeX

$$$(\operatorname{Finset.Ici}\ a).\mathrm{image}\ \mathrm{val} = \operatorname{Finset.Ico}(a.\mathrm{val}, n)$$$

Lean4

@[simp]
theorem finsetImage_val_Ici : (Ici a).image val = Ico (a : ℕ) n := by simp [← coe_inj]

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

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

Разделы

Аффилиация

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