Commit 2023-10-24 13:49 bca93b9f

View on Github →

feat: add Fin.cons_mem_piFinset_iff (#6605) Adds a lemma about when Fin.cons is an element of piFinset

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.eq_castSucc_or_eq_last

added theorem Fin.forall_fin_succ'

Modified Mathlib/Data/Fintype/Pi.lean

added theorem Fin.cons_mem_piFinset_cons_iff

added theorem Fin.mem_piFinset_succ_iff'

added theorem Fin.mem_piFinset_succ_iff

added theorem Fin.snoc_mem_piFinset_snoc_iff