OAI/Combinatorics/HadwigerCounterexample/IndependentColumnBatches.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Independent Column Batches

  1. theorem OAI.HadwigerCounterexample.joint_map line 15
  2. def OAI.HadwigerCounterexample.rawC line 24
  3. def OAI.HadwigerCounterexample.peer line 25
  4. theorem OAI.HadwigerCounterexample.peer_cap line 28
  5. abbrev OAI.HadwigerCounterexample.Forum line 52
  6. def OAI.HadwigerCounterexample.forumLaw line 53
  7. abbrev OAI.HadwigerCounterexample.NomQuery line 56
  8. def OAI.HadwigerCounterexample.peekR line 59
  9. def OAI.HadwigerCounterexample.database line 62
  10. theorem OAI.HadwigerCounterexample.law_peekR line 65
  11. abbrev OAI.HadwigerCounterexample.Ports line 88

    Source documentation

    Merge two endpoints of raw frame. Assign ports according to their endpoint.

    abbrev Ports (p : Shape) := Bool × Comp p.g

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Comp

  12. def OAI.HadwigerCounterexample.mergeR line 89
  13. theorem OAI.HadwigerCounterexample.law_mergeR line 96