[Merged by Bors] - feat: a product of indicators is the indicator of the product#17964
[Merged by Bors] - feat: a product of indicators is the indicator of the product#17964YaelDillies wants to merge 4 commits intomasterfrom
Conversation
YaelDillies
commented
Oct 20, 2024
PR summary a16521e9bd
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.BigOperators.Pi | 532 | 534 | +2 (+0.38%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Algebra.Order.Star.Conjneg Mathlib.Algebra.Star.Conjneg |
1 |
Mathlib.Algebra.BigOperators.Pi |
2 |
Declarations diff
+ mem_inf'
+ mem_sup'
+ prod_indicator
+ prod_indicator_apply
+ prod_indicator_const
+ prod_indicator_const_apply
+ prod_sub
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
| Authors: Simon Hudon, Patrick Massot | ||
| -/ | ||
| import Mathlib.Algebra.BigOperators.Group.Finset | ||
| import Mathlib.Algebra.BigOperators.GroupWithZero.Finset |
There was a problem hiding this comment.
I was gonna ask Yaël if this was okay, but I guess it is 😅
There was a problem hiding this comment.
Algebra.BigOperators.Pi hasn't yet been split up according to Group/GroupWithZero/Ring, so I just don't care yet 😁
|
(No need to block on me giving this another look) |
| · obtain ⟨i, hi, hj⟩ := by simpa using hj | ||
| exact Finset.prod_eq_zero hi <| Set.indicator_of_not_mem hj _ | ||
|
|
||
| lemma prod_indicator (s : Finset ι) (f : ι → Set κ) (g : ι → κ → α) : |
There was a problem hiding this comment.
Can you also add the version of this where f is constant (for rewrite chains, so the rhs is nice)
There was a problem hiding this comment.
I think you did the g constant one instead... Oh well
There was a problem hiding this comment.
Oh sorry! But the constant f version already has other lemmas for it
There was a problem hiding this comment.
Actually looks like we have Finset.indicator_sum and Finset.mulIndicator_prod, but not Finset.indicator_prod.
There was a problem hiding this comment.
Can you elaborate on this? The commented line does contain the statement. It includes f, in particular it includes the f which I wanted you to make constant. Is there a reason that g is more noticeable here than f?
There was a problem hiding this comment.
I mean, my advice above is a general advice. But here specifically I thought "Ah! Bhavik wants me to make the function constant" and I didn't think of f as the function (because it's set-valued) but g instead (because it's function-valued)
There was a problem hiding this comment.
I'm still not quite sure I follow. The line I highlighted was a deliberate choice, because it's where f is declared. The function f is a set-valued function, which is the one I wanted you to make constant. What would you have preferred here? Is there a way you'd prefer me to refer to a function other than by its name and pointing to the place where it's declared?
There was a problem hiding this comment.
Yes, you can comment on all the lines of the statement. Here L. 75-76. Multiline comments have been available on github for the past 2-3 years or so
There was a problem hiding this comment.
Just to clarify, your advice here is that it's less ambiguous to refer to changing the type of a function if I additionally highlight things which are not the type of the function? And that referring to an input f by its name and declaration line is not sufficiently clear, and you'd prefer seeing things other than inputs in a suggestion to amend an input?
Can you clarify why you'd prefer this? And could you explain where the ambiguity arises, for my future reference? If there is a way to refer to a variable in a lemma by something other than its name and type, I would be very happy to hear it.
I appreciate the information about multiline comments on github, indeed I have been using them for the last 4-5 years or so.
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
|
Pull request successfully merged into master. Build succeeded: |