OAI/GroupTheory/FiniteType/PosetTransport.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PosetTransport.Cocycle line 21
  2. lemma OAI.PosetTransport.Cocycle.ext line 26
  3. def OAI.PosetTransport.Cocycle.Potential line 36
  4. def OAI.PosetTransport.Cocycle.Trivial line 37
  5. def OAI.PosetTransport.Cocycle.pull line 38
  6. lemma OAI.PosetTransport.Cocycle.trivial_pull line 42
  7. lemma OAI.PosetTransport.Cocycle.square line 45
  8. lemma OAI.PosetTransport.Cocycle.trivial_compare line 49
  9. lemma OAI.PosetTransport.Cocycle.trivial_compare_rev line 57
  10. lemma OAI.PosetTransport.Cocycle.trivial_of_top line 68
  11. lemma OAI.PosetTransport.Cocycle.trivial_of_bottom line 73
  12. def OAI.PosetTransport.Adj line 77
  13. def OAI.PosetTransport.Connected line 78
  14. lemma OAI.PosetTransport.Connected.constant line 80
  15. lemma OAI.PosetTransport.connected_of_bottom line 86
  16. lemma OAI.PosetTransport.connected_of_top line 90
  17. theorem OAI.PosetTransport.Cocycle.trivial_of_lower_fibers line 95
  18. lemma OAI.PosetTransport.connected_of_constant line 115
  19. lemma OAI.PosetTransport.Connected.of_orderIso line 137
  20. theorem OAI.PosetTransport.Cocycle.trivial_of_upper_fibers line 143
  21. def OAI.PosetTransport.rankAbove line 169
  22. def OAI.PosetTransport.rankEmbed line 170
  23. def OAI.PosetTransport.rankStep line 174
  24. def OAI.PosetTransport.rankFiberIso line 178
  25. theorem OAI.PosetTransport.Cocycle.trivial_rank_step line 195
  26. theorem OAI.PosetTransport.Cocycle.trivial_of_rank line 216
  27. def OAI.PosetTransport.rankBelow line 233
  28. def OAI.PosetTransport.belowEmbed line 234
  29. def OAI.PosetTransport.belowStep line 236
  30. def OAI.PosetTransport.linkBelow line 238
  31. def OAI.PosetTransport.Cocycle.linkPotential line 246
  32. lemma OAI.PosetTransport.Cocycle.linkPotential_spec line 248
  33. def OAI.PosetTransport.Cocycle.nextEdge line 252
  34. lemma OAI.PosetTransport.Cocycle.nextEdge_old line 261
  35. lemma OAI.PosetTransport.Cocycle.nextEdge_refl line 266
  36. lemma OAI.PosetTransport.Cocycle.nextEdge_comp line 272
  37. def OAI.PosetTransport.Cocycle.next line 302
  38. lemma OAI.PosetTransport.Cocycle.next_pull line 306
  39. lemma OAI.PosetTransport.connected_of_directed line 314
  40. theorem OAI.PosetTransport.Cocycle.trivial_of_directed line 319
  41. def OAI.PosetTransport.Cocycle.extension line 340
  42. def OAI.PosetTransport.Cocycle.extensionLabel line 344
  43. lemma OAI.PosetTransport.Cocycle.extensionLabel_succ line 347
  44. lemma OAI.PosetTransport.Cocycle.extensionLabel_stable line 353
  45. def OAI.PosetTransport.Cocycle.fullExtension line 363
  46. lemma OAI.PosetTransport.Cocycle.fullExtension_pull line 373
  47. theorem OAI.PosetTransport.Cocycle.trivial_sublevel line 382
  48. lemma OAI.PosetTransport.connected_of_exactIn line 393