Commit 2025-02-27 20:21 12e9e6d9

feat: introduce a predicate DependsOn (#22191) When dealing with a function f : Π i, α i depending on many variables, some operations may get rid of the dependency on some variables (see Function.updateFinset or MeasureTheory.lmarginal for example). However considering this new function as having a different domain can lead to tedious writing. On the other hand one wants to be able for example to call some function constant with respect to some variables and be able to infer this when applying transformations mentioned above. This PR introduces the predicate DependsOn f s, which states that if x and y coincide over the set s, then f x = f y.