succAbove_left_injective

Mathlib.Data.Fin.SuccPred

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

← MathLib Explorer

English

`succAbove` is injective as a function from Fin(n) to Fin(n+1).

Русский

`succAbove` инъективна как функция из Fin(n) в Fin(n+1).

LaTeX

$$$\forall n \in \mathbb{N},\ \mathrm{Injective}(\mathrm{succAbove}).$$$

Lean4

/-- `succAbove` is injective at the pivot -/
theorem succAbove_left_injective : Injective (@succAbove n) := fun _ _ h => by
  simpa [range_succAbove] using congr_arg (fun f : Fin n → Fin (n + 1) => (Set.range f)ᶜ) h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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