add missing back-tick for not_exists definition to fix rendering issue
fix variable name in sum description to match goal
Also, I think you might not be quite consistent with the upper bounds for sums in various descriptions. Perhaps that's to keep it simpler as 0 to n instead of 0 to n-1 when not relevant. It was only slightly confusing, as someone who's just learning Lean.
I guess this is still work in progress but I thought it was quite good already (I've done all but the last 4 levels in the SetTheory world so far).
abentkamp
commented
1 year ago
not_existsdefinition to fix rendering issueAlso, I think you might not be quite consistent with the upper bounds for sums in various descriptions. Perhaps that's to keep it simpler as
0 to ninstead of0 to n-1when not relevant. It was only slightly confusing, as someone who's just learning Lean.I guess this is still work in progress but I thought it was quite good already (I've done all but the last 4 levels in the SetTheory world so far).