OAI/Combinatorics/HadwigerCounterexample/FiniteDualSystems.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Finite Dual Systems

  1. structure OAI.HadwigerCounterexample.StatusAnalysis.Zodiac line 16

    Source documentation

    envelope information to certify a generator, shared l and q.

    structure Zodiac (p : Shape) where
…

    Mentions: OAI.HadwigerCounterexample.Shape

  2. def OAI.HadwigerCounterexample.StatusAnalysis.Zodiac.aspect line 23
  3. def OAI.HadwigerCounterexample.StatusAnalysis.Zodiac.common line 25
  4. instance OAI.HadwigerCounterexample.StatusAnalysis.zodiac_dec line 27
  5. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Terrain line 29
  6. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Gazette line 30
  7. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.wisp line 36
  8. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.wake line 38
  9. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.parcelOrg line 41
  10. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.origami line 43
  11. structure OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.reports line 45
  12. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.playbook line 53
  13. theorem OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.playbook_pos line 55
  14. theorem OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.booklet_cap line 56
  15. theorem OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.plume_reports line 67
  16. abbrev OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.Scriptum line 84
  17. abbrev OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.Touch line 86
  18. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.couplePage line 89
  19. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.circlet line 91
  20. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.eligible line 93
  21. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.stellar line 96
  22. theorem OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.circlet_state line 104
  23. theorem OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.sturdy_contact line 121