castLEOrderEmb — Mathlib

English

castLEOrderEmb (h) is an order-embedding from Fin n to Fin m when h : n ≤ m.

Русский

castLEOrderEmb(h) — вложение по порядку Fin n в Fin m при условии h : n ≤ m.

LaTeX

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

Lean4

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

`castLEEmb h i` embeds `i` into a larger `Fin` type. -/
@[simps! apply toEmbedding]
def castLEOrderEmb (h : n ≤ m) : Fin n ↪o Fin m :=
  .ofStrictMono (castLE h) (strictMono_castLE h)

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