English
Take p at index i returns the initial segment of p of length i; its length is i and its elements agree with p on the first i positions.
Русский
Взять префикс p на позиции i возвращает начальный фрагмент p длины i; его длина равна i, и элементы совпадают с p на первых i позициях.
LaTeX
$$$$ \\operatorname{length}(\\mathrm{take}(p,i)) = i \\quad \\land \\quad \\forall j: \\mathsf{Fin}(i),\\ \\mathrm{take}(p,i)_{j} = p_{j}. $$$$
Lean4
/-- Given the series `a₀ -r→ … -r→ aᵢ -r→ … -r→ aₙ`, the series `a₀ -r→ … -r→ aᵢ`. -/
@[simps! length]
def take {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)) : RelSeries r
where
length := i
toFun := fun ⟨j, h⟩ => p.toFun ⟨j, by omega⟩
step := fun ⟨j, h⟩ => p.step ⟨j, by omega⟩
