tail_ofSeq — Mathlib

English

The tail of a sequence encoded by ofSeq s equals the ofSeq of s.tail.

Русский

Хвост последовательности, кодированной как ofSeq s, равен ofSeq s.tail.

LaTeX

$$$$\forall s:\\mathrm{Seq}\,\alpha,\ \mathrm{tail}(\\mathrm{ofSeq}\,s) = \\mathrm{ofSeq}\,s.tail.$$$$

Lean4

@[simp]
theorem tail_ofSeq (s : Seq α) : tail (ofSeq s) = ofSeq s.tail :=
  by
  simp only [tail, destruct_ofSeq, map_pure', flatten_pure]
  induction s using Seq.recOn <;>
    simp only [ofSeq, Seq.tail_nil, Seq.head_nil, Option.map_none, Seq.tail_cons, Seq.head_cons, Option.map_some]
  · rfl

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