get?_ofSeq — Mathlib

English

For every s : Seq α and n ∈ ℕ, get? (ofSeq s) n equals Computation.pure (Seq.get? s n).

Русский

Для любой последовательности s : Seq α и натурального n получаемый элемент get? от ofSeq s на позиции n равен Computation.pure (Seq.get? s n).

LaTeX

$$$$ \\mathrm{get?}(\\mathrm{ofSeq}(s))\\, n = \\mathrm{pure}(\\mathrm{Seq.get?}(s,n)) $$$$

Lean4

theorem get?_ofSeq (s : Seq α) (n) : get? (ofSeq s) n = Computation.pure (Seq.get? s n) := by dsimp [get?];
  rw [dropn_ofSeq, head_ofSeq, Seq.head_dropn]

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