OAI/GroupTheory/FiniteType/OrderChainsOnSet.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrderChains.onSet line 20
  2. lemma OAI.OrderChains.onSet_mono line 22
  3. lemma OAI.OrderChains.onSet_le_module line 24
  4. lemma OAI.OrderChains.boundary_onSet line 26
  5. lemma OAI.OrderChains.map_onSet line 31
  6. def OAI.OrderChains.ExactSet line 51
  7. def OAI.OrderChains.project line 55
  8. lemma OAI.OrderChains.project_val line 58
  9. lemma OAI.OrderChains.project_include line 62
  10. lemma OAI.OrderChains.exactSet_of_subtype line 65
  11. lemma OAI.OrderChains.cone_onSet_top line 86
  12. lemma OAI.OrderChains.exactSet_of_top line 97
  13. def OAI.OrderChains.cycleFill line 103
  14. lemma OAI.OrderChains.cycleFill_spec line 107
  15. lemma OAI.OrderChains.exactSet_of_bottom line 118
  16. lemma OAI.OrderChains.Descending.comparable line 126
  17. theorem OAI.OrderChains.carrier_move line 144
  18. def OAI.OrderChains.deleteCarrier line 249
  19. def OAI.OrderChains.starCarrier line 252
  20. lemma OAI.OrderChains.Descending.above_min line 255
  21. lemma OAI.OrderChains.deleteCarrier_face line 263
  22. lemma OAI.OrderChains.starCarrier_face line 277
  23. theorem OAI.OrderChains.delete_minimal line 291
  24. theorem OAI.OrderChains.delete_finite_minimal line 344