succAboveEmb

Mathlib.Data.Fin.Embedding

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

← MathLib Explorer

English

succAboveEmb(p) gives an embedding Fin n → Fin (n+1), mapping i to i.succAbove.

Русский

succAboveEmb(p) задаёт вложение Fin n → Fin(n+1), переводя i в i.succAbove.

LaTeX

$$$ \mathrm{succAboveEmb}(p) : \mathrm{Fin}(n) \hookrightarrow \mathrm{Fin}(n+1)$$$

Lean4

/-- `Fin.succAbove p` as an `Embedding`. -/
@[simps!]
def succAboveEmb (p : Fin (n + 1)) : Fin n ↪ Fin (n + 1) :=
  ⟨p.succAbove, succAbove_right_injective⟩

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

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

Разделы

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

Аффилиация

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