succAboveOrderEmb — Mathlib

English

Let p ∈ Fin(n+1). The map i ↦ succAbove p i embeds Fin(n) into Fin(n+1) in an order-preserving way: each i is mapped to the successor structure above p.

Русский

Пусть p ∈ Fin(n+1). Отображение i ↦ succAbove p i образует упорядоченное вложение Fin(n) в Fin(n+1).

LaTeX

$$$\text{succAboveOrderEmb}(p):\; \mathrm{Fin}(n) \hookrightarrow_{\mathrm{ord}} \mathrm{Fin}(n+1).$$$

Lean4

/-- `Fin.succAbove p` as an `OrderEmbedding`. -/
@[simps! apply toEmbedding]
def succAboveOrderEmb (p : Fin (n + 1)) : Fin n ↪o Fin (n + 1) :=
  OrderEmbedding.ofStrictMono (succAbove p) (strictMono_succAbove p)

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