exists_succ_eq_of_ne_zero

Mathlib.Data.Fin.SuccPred

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

English

If x ≠ 0, there exists y with y.succ = x.

Русский

Если x ≠ 0, существует y, такой что y.succ = x.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\; x \\in \\mathrm{Fin}(n+1):\\; x \\neq 0 \\Rightarrow \\exists y, y.{\\mathrm{succ}} = x$$$

Lean4

theorem exists_succ_eq_of_ne_zero {x : Fin (n + 1)} (h : x ≠ 0) : ∃ y, Fin.succ y = x :=
  exists_succ_eq.mpr h

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

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

Разделы

Аффилиация

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