castAddOrderEmb — Mathlib

English

castAddOrderEmb m i embeds i : Fin n into Fin (n+m) as an order-embedding.

Русский

castAddOrderEmb m i отображает i : Fin n в Fin (n+m) как вложение по порядку.

LaTeX

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

Lean4

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

`castAddEmb m i` embeds `i : Fin n` in `Fin (n+m)`. See also `Fin.natAddEmb` and `Fin.addNatEmb`. -/
@[simps! apply toEmbedding]
def castAddOrderEmb (m) : Fin n ↪o Fin (n + m) :=
  .ofStrictMono (castAdd m) (strictMono_castAdd m)

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