insertNth_left_injective

Mathlib.Data.Fin.Tuple.Basic

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

← MathLib Explorer

English

For fixed p, the map x ↦ p.insertNth x is injective.

Русский

Для фиксированного p отображение x ↦ p.insertNth x является инъективным.

LaTeX

$$∀ p, \text{Injective}(\lambda x. p.insertNth x)$$

Lean4

theorem insertNth_left_injective {p : Fin (n + 1)} (x : ∀ i, α (succAbove p i)) :
    Function.Injective (insertNth p · x) :=
  insertNth_injective2.left _

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

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

Разделы

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

Аффилиация

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