OAI/GroupTheory/FiniteType/OrderChains.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrderChains.Descending line 20
  2. def OAI.OrderChains.module line 21
  3. def OAI.OrderChains.carrier line 22
  4. lemma OAI.OrderChains.Descending.le_head line 24
  5. lemma OAI.OrderChains.Descending.boundary line 29
  6. lemma OAI.OrderChains.carrier_le_module line 32
  7. lemma OAI.OrderChains.carrier_mono line 33
  8. lemma OAI.OrderChains.cone_carrier line 35
  9. lemma OAI.OrderChains.boundary_mem line 49
  10. lemma OAI.OrderChains.Descending.map line 55
  11. lemma OAI.OrderChains.Descending.map_carrier line 59
  12. lemma OAI.OrderChains.map_mem line 70
  13. lemma OAI.OrderChains.map_degree line 75
  14. def OAI.OrderChains.comparison line 85
  15. lemma OAI.OrderChains.comparison_boundary line 88
  16. lemma OAI.OrderChains.comparison_mem line 96
  17. lemma OAI.OrderChains.comparison_degree line 114
  18. lemma OAI.OrderChains.mapChain_comp line 128
  19. lemma OAI.OrderChains.mapChain_id line 136
  20. def OAI.OrderChains.ExactIn line 143
  21. theorem OAI.OrderChains.exactIn_of_comparison line 147
  22. lemma OAI.OrderChains.exactIn_of_orderIso line 169
  23. def OAI.SteinChains.ProperFace line 177
  24. instance OAI.SteinChains.(instance at line 178) line 178
  25. def OAI.SteinChains.properInclude line 180
  26. def OAI.SteinChains.properProject line 184
  27. lemma OAI.SteinChains.properProject_val line 194
  28. lemma OAI.SteinChains.project_include line 198
  29. lemma OAI.SteinChains.properInclude_mem line 203
  30. lemma OAI.SteinChains.properProject_mem line 221
  31. theorem OAI.SteinChains.properFace_exactIn line 242