toSeq_ofSeq — Mathlib

English

The operation toSeq is the inverse of ofSeq on sequences: for any s, toSeq(ofSeq s) = s.

Русский

Операции toSeq и ofSeq образуют взаимно обратные преобразования: для любой последовательности s, toSeq(ofSeq s) = s.

LaTeX

$$$$ \mathrm{toSeq}(\mathrm{ofSeq}(s)) = s. $$$$

Lean4

theorem toSeq_ofSeq (s : Seq α) : toSeq (ofSeq s) = s :=
  by
  apply Subtype.eq; funext n
  dsimp [toSeq]; apply get_eq_of_mem
  rw [get?_ofSeq]; apply ret_mem

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