Commit 2025-11-27 08:19 4c04a1de

View on Github →

feat(Data/Finsupp/Basic): Finsupp.optionElim (#25920) Similar to how Finsupp.cons constructs a map Fin (n + 1) →₀ M from a map Fin n →₀ M, we define Finsupp.optionElim' to construct a map Option α →₀ M from a map α →₀ M, given an additional value for none. We base this on the new optionEquiv definition. As a function, it behaves as Option.elim', hence the name. We prove a variety of API lemmas, based on those for Finsupp.cons, to bring the definitions more in line with the contents of Data/Finsupp/Fin. Original PR: https://github.com/leanprover-community/mathlib4/pull/13861

depends on: #26309

Estimated changes

Modified Mathlib/Data/Finsupp/Option.lean

modified theorem Finsupp.embDomain_some_none

modified theorem Finsupp.embDomain_some_some

modified theorem Finsupp.eq_option_embedding_update_none_iff

added def Finsupp.optionElim

added theorem Finsupp.optionElim_apply_eq_elim

added theorem Finsupp.optionElim_apply_none

added theorem Finsupp.optionElim_apply_some

added theorem Finsupp.optionElim_eq_elim'

added theorem Finsupp.optionElim_ne_zero_iff

added theorem Finsupp.optionElim_ne_zero_of_left

added theorem Finsupp.optionElim_ne_zero_of_right

added theorem Finsupp.optionElim_some

added theorem Finsupp.optionElim_zero

modified def Finsupp.some

modified theorem Finsupp.some_apply

modified theorem Finsupp.some_embDomain_some

added theorem Finsupp.some_optionElim

modified theorem Finsupp.some_single_none

modified theorem Finsupp.some_single_some

modified theorem Finsupp.some_update_none

modified theorem Finsupp.some_zero