coe_succAboveEmb

Mathlib.Data.Fin.Embedding

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

English

For every p in Fin(n+1), the two notions succAboveEmb and succAbove coincide: p.succAboveEmb = p.succAbove.

Русский

Для каждого p в Fin(n+1) обладают равенством: p.succAboveEmb = p.succAbove.

LaTeX

$$$\forall p : \mathrm{Fin}(n+1),\ p.succAboveEmb = p.succAbove$$$

Lean4

@[simp, norm_cast]
theorem coe_succAboveEmb (p : Fin (n + 1)) : p.succAboveEmb = p.succAbove :=
  rfl

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

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

Разделы

Аффилиация

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