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 _