castSuccOrderEmb — Mathlib

English

castSuccOrderEmb is an order-embedding from Fin n to Fin (n+1).

Русский

castSuccOrderEmb является вложением по порядку Fin n в Fin(n+1).

LaTeX

$$$\forall {n : \mathbb{N}}, Fin n \hookrightarrow^o Fin (n + 1)$$$

Lean4

/-- `Fin.castSucc` as an `OrderEmbedding`.

`castSuccOrderEmb i` embeds `i : Fin n` in `Fin (n+1)`. -/
@[simps! apply toEmbedding]
def castSuccOrderEmb : Fin n ↪o Fin (n + 1) :=
  .ofStrictMono castSucc strictMono_castSucc

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