Commit 2024-04-25 04:21 d700199f

View on Github →

feat(List/Enum): add lemmas (#11969)

Estimated changes

Modified Mathlib/Data/List/Enum.lean

deleted theorem List.enumFrom_get?

deleted theorem List.enum_get?

modified theorem List.enum_map_snd

added theorem List.fst_lt_add_of_mem_enumFrom

added theorem List.fst_lt_of_mem_enum

added theorem List.get?_enum

added theorem List.get?_enumFrom

modified theorem List.get_enum

modified theorem List.get_enumFrom

added theorem List.le_fst_of_mem_enumFrom

modified theorem List.mem_enumFrom

added theorem List.mem_enum_iff_get?

added theorem List.mk_add_mem_enumFrom_iff_get?

added theorem List.mk_mem_enumFrom_iff_le_and_get?_sub

added theorem List.mk_mem_enum_iff_get?

added theorem List.snd_mem_of_mem_enum

added theorem List.snd_mem_of_mem_enumFrom