Skip to content

Commit e503193

Browse files
committed
chore(Combinatorics/Enumerative/InclusionExclusion): remove solved TODO
1 parent b16b285 commit e503193

1 file changed

Lines changed: 0 additions & 4 deletions

File tree

Mathlib/Combinatorics/Enumerative/InclusionExclusion.lean

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -37,10 +37,6 @@ Per the above explanation, this file contains the following variants of inclusio
3737
3838
See also `MeasureTheory.integral_biUnion_eq_sum_powerset` for the version with integrals, and
3939
`MeasureTheory.measureReal_biUnion_eq_sum_powerset` for the version with measures.
40-
41-
## TODO
42-
43-
* Prove that truncating the series alternatively gives an upper/lower bound to the true value.
4440
-/
4541

4642
public section

0 commit comments

Comments
 (0)