map_castSuccEmb_Ici

Mathlib.Order.Interval.Finset.Fin

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

English

For i ∈ Fin n, the image of Ici i under castSuccEmb equals Ico i.castSucc (last n).

Русский

Для i ∈ Fin n образ Ici i под castSuccEmb равен Ico i.castSucc (last n).

LaTeX

$$$$(\\mathrm{Finset.map}\\;\\operatorname{castSuccEmb})\\ (\\mathrm{Ici}\\ i) = \\mathrm{Ico}(i.castSucc, \\mathrm{last}\\ n)$$$$

Lean4

@[simp]
theorem map_castSuccEmb_Ici (i : Fin n) : (Ici i).map castSuccEmb = Ico i.castSucc (.last n) :=
  map_castAddEmb_Ici ..

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

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

Разделы

Аффилиация

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