castSuccEmb

Mathlib.Data.Fin.Embedding

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

English

Succ as an embedding: Fin n ↪ Fin (n+1) given by adding one to the index.

Русский

Succ как вложение: Fin n ↪ Fin(n+1) задано добавлением единицы к индексу.

LaTeX

$$$ castSuccEmb : Fin n \hookrightarrow Fin (n+1) $$$

Lean4

/-- `Fin.castSucc` as an `Embedding`, `castSuccEmb i` embeds `i : Fin n` in `Fin (n+1)`. -/
def castSuccEmb : Fin n ↪ Fin (n + 1) :=
  castAddEmb _

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

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

Разделы

Аффилиация

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