Commit 2023-11-07 13:59 0eb6b931

View on Github →

feat: define updateFinset which updates a finite number components of a vector (#7341)

from the Sobolev project (formerly: marginal project)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finset/Basic.lean

added def Equiv.Finset.union

added theorem Equiv.Finset.union_symm_inl

added theorem Equiv.Finset.union_symm_inr

added def Equiv.piFinsetUnion

added theorem Finset.coe_disjUnion

added theorem Finset.default_singleton

Created Mathlib/Data/Finset/Update.lean

added def Function.updateFinset

added theorem Function.updateFinset_empty

added theorem Function.updateFinset_singleton

added theorem Function.updateFinset_updateFinset

added theorem Function.update_eq_updateFinset

Modified Mathlib/Data/Set/Prod.lean

added theorem Set.uniqueElim_preimage

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.pred_update

Modified Mathlib/Logic/Unique.lean

added def uniqueElim

added theorem uniqueElim_default