Commit 2024-11-18 14:56 5ebc4a6a

View on Github →

feat(Data/seq): basic lemmas about Stream'.seq and the definition of length (#18589)

Estimated changes

Modified Mathlib/Data/Seq/Seq.lean

added theorem Stream'.Seq.get?_zero_eq_none

added theorem Stream'.Seq.getElem?_take

added theorem Stream'.Seq.getElem?_toList

added theorem Stream'.Seq.getLast?_toList

added def Stream'.Seq.length

added theorem Stream'.Seq.length_eq_zero

added theorem Stream'.Seq.length_le_iff'

added theorem Stream'.Seq.length_le_iff

added theorem Stream'.Seq.length_map

added theorem Stream'.Seq.length_nil

added theorem Stream'.Seq.length_take_of_le_length

added theorem Stream'.Seq.length_toList

added theorem Stream'.Seq.lt_length_iff'

added theorem Stream'.Seq.lt_length_iff

added theorem Stream'.Seq.ofList_injective

added theorem Stream'.Seq.ofList_toList

added theorem Stream'.Seq.terminatedAt_map_iff

added theorem Stream'.Seq.terminatedAt_nil

added theorem Stream'.Seq.terminatedAt_ofList

added theorem Stream'.Seq.terminatedAt_zero_iff

added theorem Stream'.Seq.terminates_map_iff

added theorem Stream'.Seq.terminates_nil

added theorem Stream'.Seq.terminates_ofList

added theorem Stream'.Seq.toList_nil

added theorem Stream'.Seq.toList_ofList