Commit 2025-08-24 19:45 ab7db0b0

View on Github →

feat(Data/Seq): update and set operations for Seq (#26120) Introduce update and set operations for sequences, along with a few lemmas about them.

Estimated changes

Modified Mathlib/Data/Seq/Seq.lean

added theorem Stream'.Seq.drop_set_of_lt

added theorem Stream'.Seq.get?_set_of_ne

added theorem Stream'.Seq.get?_set_of_not_terminatedAt

added theorem Stream'.Seq.get?_set_of_terminatedAt

added theorem Stream'.Seq.get?_update

added def Stream'.Seq.set

added theorem Stream'.Seq.set_cons_succ

added theorem Stream'.Seq.set_cons_zero

added theorem Stream'.Seq.set_nil

added def Stream'.Seq.update

added theorem Stream'.Seq.update_cons_succ

added theorem Stream'.Seq.update_cons_zero

added theorem Stream'.Seq.update_nil