John Hughes (Jul 03 2025 at 14:01): John Hughes (Jul 03 2025 at 14:01):I'd very much like to take a sum over a small finite set. I've tried writing this:
lemma j:
fixes S::"nat set set"
assumes "card S = 3"
assumes "T ∈ S ⟹ card T = 2"
shows "6 = ∑ T ∈ S . card T"
but I get an error message (inner syntax error) at the ∈ .
I've looked at the definition of ∑ and it seems to allow this notation, but apparently I'm misunderstanding.
Can you show me how to fix this theorem statement? (I'm hoping that proving it will be relatively easy!)
Lukas Stevens (Jul 03 2025 at 14:04):You need to put parentheses around the right-hand side to delimit the binder, i.e. (∑ T ∈ S . card T).
John Hughes (Jul 03 2025 at 14:09):Thank you so much... I knew it had to be something simple!
Manuel Eberl (Jul 08 2025 at 09:53):That's a general rule: any syntax that binds a variable should have parentheses around it. The same also applies for mixfix syntax like if then else and case. Some exceptions apply (e.g. nested sums), but it's a good rule of thumb.
Last updated: Jul 12 2025 at 12:41 UTC