range_succ

Mathlib.Data.Fin.SuccPred

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

English

The image of Fin.succ is exactly the set of all elements of Fin(n+1) except 0.

Русский

Образ Fin.succ равен всем элементам Fin(n+1) кроме 0.

LaTeX

$$$\forall n \in \mathbb{N},\ \mathrm{set.range}(\mathrm{Fin}.\mathrm{succ}) = \{0\}^{c}.$$$

Lean4

@[simp]
theorem range_succ (n : ℕ) : Set.range (Fin.succ : Fin n → Fin (n + 1)) = {0}ᶜ := by
  rw [← succAbove_zero, range_succAbove]

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

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

Разделы

Аффилиация

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