castLEEmb — Mathlib

English

For any h with n ≤ m, there is an embedding Fin n → Fin m given by castLE h.

Русский

Для любого h с n ≤ m существует вложение Fin n → Fin m, заданное castLE h.

LaTeX

$$$ castLEEmb(h) : Fin(n) \hookrightarrow Fin(m)$$$

Lean4

/-- `Fin.castLE` as an `Embedding`, `castLEEmb h i` embeds `i` into a larger `Fin` type. -/
@[simps apply]
def castLEEmb (h : n ≤ m) : Fin n ↪ Fin m where
  toFun := castLE h
  inj' := castLE_injective _

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