ne_succAbove

Mathlib.Data.Fin.SuccPred

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

English

For all p ∈ Fin(n+1) and i ∈ Fin(n), p.succAbove(i) ≠ p.

Русский

Для всех p ∈ Fin(n+1) и i ∈ Fin(n) верно, что p.succAbove(i) ≠ p.

LaTeX

$$$\forall p \in \mathrm{Fin}(n+1),\ \forall i \in \mathrm{Fin}(n),\ p.succAbove(i) \neq p.$$$

Lean4

@[simp]
theorem ne_succAbove (p : Fin (n + 1)) (i : Fin n) : p ≠ p.succAbove i :=
  (succAbove_ne _ _).symm

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

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

Разделы

Аффилиация

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