OAI/Combinatorics/HadwigerCounterexample/PreparedPopulationTrimming.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.PreparationParameters.retainInitial line 17
2. abbrev OAI.HadwigerCounterexample.PreparationParameters.Campaign line 31
3. structure OAI.HadwigerCounterexample.PreparationParameters.citable line 33
4. def OAI.HadwigerCounterexample.PreparationParameters.potion line 39
5. def OAI.HadwigerCounterexample.PreparationParameters.charm line 41
6. theorem OAI.HadwigerCounterexample.PreparationParameters.citable.on_law line 44
7. theorem OAI.HadwigerCounterexample.PreparationParameters.dropHarvest line 53
8. def OAI.HadwigerCounterexample.PreparationParameters.nebulous line 103

   Source documentation

   Tiny cover exists after preparing retained mass, seen on its support. Requires each old tile contain only original support.

   def nebulous (q : PreparationParameters) (l : Filter ℕ) (s : rhythms p M) (w : tale p M) (P : Campaign p M)
       (b : Sketch p M) :=
   …

   Mentions: OAI.HadwigerCounterexample.PreparationParameters, OAI.HadwigerCounterexample.PreparationParameters.rhythms, OAI.HadwigerCounterexample.PreparationParameters.tale, OAI.HadwigerCounterexample.PreparationParameters.Campaign, OAI.HadwigerCounterexample.PreparationParameters.Sketch

9. theorem OAI.HadwigerCounterexample.PreparationParameters.hideOn line 108
10. theorem OAI.HadwigerCounterexample.PreparationParameters.pressHarvest line 126