OAI/Combinatorics/HadwigerCounterexample/OffsetRecords.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Offset Records

  1. def OAI.HadwigerCounterexample.fpAt line 13
  2. def OAI.HadwigerCounterexample.fyAt line 15
  3. def OAI.HadwigerCounterexample.imageP line 17
  4. abbrev OAI.HadwigerCounterexample.BMark line 20
  5. def OAI.HadwigerCounterexample.mrAmbient line 21
  6. def OAI.HadwigerCounterexample.delta line 23
  7. theorem OAI.HadwigerCounterexample.mr_box line 26
  8. abbrev OAI.HadwigerCounterexample.Wide line 34
  9. abbrev OAI.HadwigerCounterexample.OffBasis line 35
  10. abbrev OAI.HadwigerCounterexample.OffAux line 37
  11. abbrev OAI.HadwigerCounterexample.Atlas line 39
  12. instance OAI.HadwigerCounterexample.aFintype line 42
  13. instance OAI.HadwigerCounterexample.aDefault line 47
  14. abbrev OAI.HadwigerCounterexample.breadth line 52
  15. def OAI.HadwigerCounterexample.cells line 53
  16. abbrev OAI.HadwigerCounterexample.Batch line 55
  17. def OAI.HadwigerCounterexample.src line 58
  18. def OAI.HadwigerCounterexample.edgeCost line 61
  19. def OAI.HadwigerCounterexample.spelled line 63
  20. def OAI.HadwigerCounterexample.compFor line 69

    Source documentation

    comp for A play Zplus paired offset+, Zminus paired offset-. Companion columns at each compared sign in opposite sign primal frame.

    def compFor (X : Atlas p r S) (A : Batch X N) (C : Cov p N)
    (D : Ambient p N) :=
…

    Mentions: OAI.HadwigerCounterexample.Atlas, OAI.HadwigerCounterexample.Batch, OAI.HadwigerCounterexample.Cov, OAI.HadwigerCounterexample.Ambient

  21. def OAI.HadwigerCounterexample.locIndep line 73
  22. def OAI.HadwigerCounterexample.standard line 75
  23. theorem OAI.HadwigerCounterexample.join_order line 77
  24. theorem OAI.HadwigerCounterexample.delta_offset line 96
  25. def OAI.HadwigerCounterexample.offsetCov line 157
  26. theorem OAI.HadwigerCounterexample.offsetCov_dim line 159
  27. theorem OAI.HadwigerCounterexample.covered_spelled line 164

    Source documentation

    Capturing offsets suffices to cover the tensor.

    theorem covered_spelled (X : Atlas p r S) (A) (T : Cov p N) (he : offsetCov X ≤ T) :
    covered p T (spelled X A) := by
…

    Mentions: OAI.HadwigerCounterexample.Atlas, OAI.HadwigerCounterexample.Cov, OAI.HadwigerCounterexample.offsetCov, OAI.HadwigerCounterexample.covered, OAI.HadwigerCounterexample.spelled

  28. theorem OAI.HadwigerCounterexample.atlas_size line 182