Commit 2024-11-08 16:20 0d2ec817

View on Github →

feat: add list lemmas (#18349) Add some general purpose lemmas on lists. Also execute two adaptation notes. The lemmas are taken from https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean

Estimated changes

added theorem List.eq_nil_or_concat'
added theorem List.left_eq_take_iff
added theorem List.take_concat_get'
added theorem List.take_eq_left_iff
added theorem List.take_eq_self_iff
added theorem List.take_self_eq_iff
added theorem List.IsPrefix.drop
added theorem List.IsPrefix.take
added theorem List.map_inits
added theorem List.map_tails
added theorem List.take_inits