OAI/Combinatorics/HadwigerCounterexample/PredictionClasses.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.HadwigerCounterexample.PredictionClass line 14
2. def OAI.HadwigerCounterexample.PredictionClass.active line 24
3. def OAI.HadwigerCounterexample.PredictionClass.echoes line 30
4. def OAI.HadwigerCounterexample.PredictionClass.firstBit line 34
5. def OAI.HadwigerCounterexample.PredictionClass.lit line 36
6. def OAI.HadwigerCounterexample.PredictionClass.assembly line 40
7. def OAI.HadwigerCounterexample.PredictionClass.recital line 44

   Source documentation

   Enough to test against dual relations.

   def recital (c : PredictionClass) (p : Shape) {N}
       (g : Bool→Augur p N) (α : Party) (τ : ℝ) :=
   …

   Mentions: OAI.HadwigerCounterexample.PredictionClass, OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Augur, OAI.HadwigerCounterexample.Party

8. abbrev OAI.HadwigerCounterexample.PredictionClass.season line 48
9. def OAI.HadwigerCounterexample.PredictionClass.disappearing line 49
10. def OAI.HadwigerCounterexample.PredictionClass.modest line 52
11. def OAI.HadwigerCounterexample.PredictionClass.accords line 56
12. def OAI.HadwigerCounterexample.PredictionClass.census line 61
13. theorem OAI.HadwigerCounterexample.PredictionClass.census_active line 71
14. theorem OAI.HadwigerCounterexample.PredictionClass.census_lit line 77
15. theorem OAI.HadwigerCounterexample.PredictionClass.disappearing_add line 86
16. theorem OAI.HadwigerCounterexample.PredictionClass.census_match line 104
17. theorem OAI.HadwigerCounterexample.PredictionClass.census_echoes line 120
18. theorem OAI.HadwigerCounterexample.PredictionClass.eventual_echoes line 159
19. theorem OAI.HadwigerCounterexample.PredictionClass.examine line 172