OAI/Combinatorics/HadwigerCounterexample/SurrogateStatusLaws.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Surrogate Status Laws

  1. abbrev OAI.HadwigerCounterexample.Silhouette line 14
  2. structure OAI.HadwigerCounterexample.StatusAnalysis.Appearance line 18
  3. instance OAI.HadwigerCounterexample.StatusAnalysis.(instance at line 24) line 24
  4. def OAI.HadwigerCounterexample.StatusAnalysis.Appearance.apt line 36
  5. def OAI.HadwigerCounterexample.StatusAnalysis.Appearance.trot line 37
  6. def OAI.HadwigerCounterexample.StatusAnalysis.Appearance.wit line 38
  7. def OAI.HadwigerCounterexample.StatusAnalysis.Appearance.face line 39
  8. def OAI.HadwigerCounterexample.StatusAnalysis.Appearance.profile line 41
  9. theorem OAI.HadwigerCounterexample.StatusAnalysis.Appearance.witLaw line 44
  10. def OAI.HadwigerCounterexample.StatusAnalysis.Appearance.showTag line 48
  11. def OAI.HadwigerCounterexample.StatusAnalysis.Appearance.reference line 50
  12. def OAI.HadwigerCounterexample.StatusAnalysis.Appearance.empirical line 51
  13. def OAI.HadwigerCounterexample.StatusAnalysis.Appearance.reflected line 54
  14. theorem OAI.HadwigerCounterexample.StatusAnalysis.Appearance.reflectedLaw line 57
  15. def OAI.HadwigerCounterexample.StatusAnalysis.Appearance.close line 62
  16. theorem OAI.HadwigerCounterexample.StatusAnalysis.stained_except line 67
  17. theorem OAI.HadwigerCounterexample.StatusAnalysis.inside_color line 73
  18. theorem OAI.HadwigerCounterexample.StatusAnalysis.varError line 88
  19. theorem OAI.HadwigerCounterexample.StatusAnalysis.Appearance.close_expect line 99
  20. theorem OAI.HadwigerCounterexample.StatusAnalysis.Appearance.show_pr line 110
  21. theorem OAI.HadwigerCounterexample.StatusAnalysis.Appearance.reflection_exact line 126