OAI/Combinatorics/HadwigerCounterexample/AffineFrames.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Affine Frames

  1. structure OAI.HadwigerCounterexample.Mixer line 15
  2. abbrev OAI.HadwigerCounterexample.Pdual line 20
  3. def OAI.HadwigerCounterexample.linTensor line 22
  4. theorem OAI.HadwigerCounterexample.linTensor_val line 25
  5. def OAI.HadwigerCounterexample.T0 line 30
  6. theorem OAI.HadwigerCounterexample.T0_val line 35
  7. def OAI.HadwigerCounterexample.B1 line 40
  8. def OAI.HadwigerCounterexample.Tmix line 54
  9. def OAI.HadwigerCounterexample.Tsym line 55
  10. theorem OAI.HadwigerCounterexample.Tsym_val line 57
  11. theorem OAI.HadwigerCounterexample.T_swap line 62
  12. theorem OAI.HadwigerCounterexample.T_diag line 68
  13. def OAI.HadwigerCounterexample.grad line 72
  14. theorem OAI.HadwigerCounterexample.grad_val line 73
  15. abbrev OAI.HadwigerCounterexample.Full line 76
  16. abbrev OAI.HadwigerCounterexample.RawFrame line 77
  17. abbrev OAI.HadwigerCounterexample.Oframe line 78
  18. abbrev OAI.HadwigerCounterexample.Orient line 79
  19. def OAI.HadwigerCounterexample.primary line 81
  20. def OAI.HadwigerCounterexample.channel line 82
  21. theorem OAI.HadwigerCounterexample.fromCols_frame line 84
  22. theorem OAI.HadwigerCounterexample.primary_inj line 87
  23. def OAI.HadwigerCounterexample.valid line 100
  24. def OAI.HadwigerCounterexample.frameLaw line 105
  25. abbrev OAI.HadwigerCounterexample.Ambient line 108
  26. def OAI.HadwigerCounterexample.Uembed line 110
  27. def OAI.HadwigerCounterexample.ufun line 115
  28. theorem OAI.HadwigerCounterexample.Uembed_inj line 121
  29. theorem OAI.HadwigerCounterexample.ufun_self line 127
  30. def OAI.HadwigerCounterexample.hole line 136

    Source documentation

    Witnesses v,w are in the cut-profile space. The gradients agree over that whole space.

    def hole (m : Mixer p n) (x y : Orient p n N) :=
…

    Mentions: OAI.HadwigerCounterexample.Mixer, OAI.HadwigerCounterexample.Orient

  31. theorem OAI.HadwigerCounterexample.hole_sym line 144
  32. theorem OAI.HadwigerCounterexample.not_hole_self line 148
  33. theorem OAI.HadwigerCounterexample.hole_triangle line 153
  34. def OAI.HadwigerCounterexample.rawHoles line 185