getElemAsFin — Mathlib

English

For an m-admissible L, each index k with k < |L| gives an element of Fin(m+k+1) equal to L[k].

Русский

Для m-допустимого списка L каждый индекс k < |L| задаёт элемент Fin(m+k+1), равный L[k].

LaTeX

$$$\\\\text{If } L \\\\\\text{ is } m\\text{-admissible, then for each } k < |L|,\\\\ \\\\text{the element } L_k \\\\in Fin(m+k+1).$$$

Lean4

/-- An element of a `m`-admissible list, as an element of the appropriate `Fin` -/
@[simps]
def getElemAsFin {L : List ℕ} (hl : IsAdmissible m L) (k : ℕ) (hK : k < L.length) : Fin (m + k + 1) :=
  Fin.mk L[k] <| Nat.le_iff_lt_add_one.mp (by simp [hl.le])

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