OAI/Combinatorics/PolynomialVacuum/Separator/CenteredPartition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialVacuumCylinder.finiteSeparatorSystems line 10
2. theorem OAI.PolynomialVacuumCylinder.mem_finiteSeparatorSystems line 13
3. theorem OAI.PolynomialVacuumCylinder.bounded_separator_sum line 19
4. theorem OAI.PolynomialVacuumCylinder.neg_half_circumference line 36
5. theorem OAI.PolynomialVacuumCylinder.centered_partition_identity line 42
6. theorem OAI.PolynomialVacuumCylinder.finiteSeparatorSystems_mono line 79
7. theorem OAI.PolynomialVacuumCylinder.eventually_mem_finiteSeparatorSystems line 85