OAI/GroupTheory/FiniteType/TwistedBrinBasisFirstCut.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TwistedBrin.Basis.FirstCut line 21
  2. instance OAI.TwistedBrin.Basis.(instance at line 23) line 23
  3. def OAI.TwistedBrin.Basis.CutSelections.selected line 30
  4. lemma OAI.TwistedBrin.Basis.CutSelections.mem_selected line 33
  5. def OAI.TwistedBrin.Basis.CutSelections.fromSelected line 38
  6. lemma OAI.TwistedBrin.Basis.CutSelections.mem_fromSelected line 49
  7. lemma OAI.TwistedBrin.Basis.CutSelections.selected_fromSelected line 59
  8. lemma OAI.TwistedBrin.Basis.CutSelections.fromSelected_selected line 65
  9. def OAI.TwistedBrin.Basis.CutSelections.booleanEquiv line 77
  10. lemma OAI.TwistedBrin.Basis.grid_rank_bound line 93
  11. def OAI.TwistedBrin.Basis.ProperCutInterval line 114
  12. instance OAI.TwistedBrin.Basis.(instance at line 116) line 116
  13. def OAI.TwistedBrin.Basis.properCore line 119
  14. lemma OAI.TwistedBrin.Basis.properCore_le line 123
  15. lemma OAI.TwistedBrin.Basis.properCore_idempotent line 125
  16. def OAI.TwistedBrin.Basis.CutSelections.empty line 131
  17. def OAI.TwistedBrin.Basis.CutSelections.full line 132
  18. lemma OAI.TwistedBrin.Basis.CutSelections.selected_empty line 133
  19. lemma OAI.TwistedBrin.Basis.CutSelections.selected_full line 136
  20. lemma OAI.TwistedBrin.Basis.CutSelections.grid_eq_bottom_iff line 140
  21. lemma OAI.TwistedBrin.Basis.CutSelections.grid_eq_top_iff line 152
  22. lemma OAI.TwistedBrin.Basis.CutSelections.grid_ne_top line 163
  23. def OAI.TwistedBrin.Basis.CutSelections.Proper line 172
  24. instance OAI.TwistedBrin.Basis.CutSelections.(instance at line 173) line 173
  25. def OAI.TwistedBrin.Basis.CutSelections.properToInterval line 176
  26. def OAI.TwistedBrin.Basis.CutSelections.properOfInterval line 179
  27. lemma OAI.TwistedBrin.Basis.CutSelections.proper_of_to line 184
  28. lemma OAI.TwistedBrin.Basis.CutSelections.proper_to_of line 186
  29. def OAI.TwistedBrin.Basis.CutSelections.properBooleanBoundary line 190
  30. def OAI.TwistedBrin.Basis.CutSelections.properBooleanFaces line 204
  31. def OAI.TwistedBrin.OrderNerve.interpolation line 221
  32. def OAI.TwistedBrin.OrderNerve.cylinder line 236
  33. def OAI.TwistedBrin.OrderNerve.homotopy line 244
  34. lemma OAI.TwistedBrin.OrderNerve.nerveMap_order_id line 268
  35. lemma OAI.TwistedBrin.OrderNerve.nerveMap_order_comp line 269
  36. def OAI.TwistedBrin.OrderNerve.retractionChainEquiv line 273
  37. def OAI.TwistedBrin.Basis.properIntervalChainEquiv line 296
  38. def OAI.TwistedBrin.Basis.Elementary line 309
  39. lemma OAI.TwistedBrin.Basis.elementary_iff_firstCore line 312
  40. lemma OAI.TwistedBrin.Basis.elementary_refl line 320
  41. lemma OAI.TwistedBrin.Basis.elementary_cutRefines line 323
  42. def OAI.TwistedBrin.Pattern.FullGrid line 331
  43. lemma OAI.TwistedBrin.Pattern.fullGrid_uniform line 335
  44. lemma OAI.TwistedBrin.Pattern.FullGrid.of_pieces_eq line 344
  45. lemma OAI.TwistedBrin.Pattern.FullGrid.length_eq line 362
  46. lemma OAI.TwistedBrin.Pattern.pieces_eq_of_lengths line 380
  47. lemma OAI.TwistedBrin.Pattern.FullGrid.pieces_eq_uniform line 395
  48. lemma OAI.TwistedBrin.Pattern.FullGrid.graft_part line 406
  49. lemma OAI.TwistedBrin.Pattern.FullGrid.of_relabel line 419
  50. lemma OAI.TwistedBrin.Basis.expand_eq_of_pattern_pieces_eq line 433
  51. lemma OAI.TwistedBrin.Basis.Forest.elementary_of_fullGrid line 453
  52. lemma OAI.TwistedBrin.Basis.Forest.fullGrid_of_elementary line 459
  53. lemma OAI.TwistedBrin.Basis.elementary_upper line 465