map_addNatEmb_Ici

Mathlib.Order.Interval.Finset.Fin

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

English

The image of Ici i under addNatEmb m is Ici (i.addNat m).

Русский

Образ Ici i под addNatEmb m равен Ici (i.addNat m).

LaTeX

$$$ (Ici i).map (addNatEmb m) = Ici (i.addNat m) $$$

Lean4

@[simp]
theorem map_addNatEmb_Ici (m) (i : Fin n) : (Ici i).map (addNatEmb m) = Ici (i.addNat m) := by simp [← coe_inj]

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

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

Разделы

Аффилиация

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