OAI/SetTheory/PartitionConsistency/Construction/MonoidTowers.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Tower

  1. instance OAI.PartitionConsistency.MonoidConstruction.(instance at line 13) line 13
  2. instance OAI.PartitionConsistency.MonoidConstruction.(instance at line 21) line 21
  3. abbrev OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.Carrier line 28
  4. def OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.transition line 30
  5. instance OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.(instance at line 33) line 33
  6. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.conservative line 41
  7. abbrev OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.Limit line 44
  8. def OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.old line 46
  9. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.old_map line 48
  10. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.old_e line 52
  11. def OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.margin line 57
  12. def OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.object line 63
  13. def OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.inclusion line 74
  14. def OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.cocone line 84
  15. def OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.liftFun line 96
  16. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.lift_old line 102
  17. def OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.liftMonoidHom line 104
  18. theorem OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.lift_conservative line 119
  19. def OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.lift line 147
  20. def OAI.PartitionConsistency.MonoidConstruction.DirectedColimit.isColimit line 161
  21. instance OAI.PartitionConsistency.MonoidConstruction.(instance at line 172) line 172
  22. def OAI.PartitionConsistency.ConstructionIteration.pairCocone line 191
  23. def OAI.PartitionConsistency.ConstructionIteration.isColimitPair line 201
  24. def OAI.PartitionConsistency.ConstructionIteration.isColimitFst line 210
  25. def OAI.PartitionConsistency.ConstructionIteration.isColimitSnd line 219
  26. instance OAI.PartitionConsistency.ConstructionIteration.(instance at line 228) line 228
  27. instance OAI.PartitionConsistency.ConstructionIteration.(instance at line 233) line 233
  28. instance OAI.PartitionConsistency.ConstructionIteration.(instance at line 236) line 236
  29. structure OAI.PartitionConsistency.ConstructionIteration.Step line 244

    Source documentation

    Stage-indexed iteration. The second factor records the actual stage; limits take its supremum, rather than skipping pending operations.

    structure Step {C : Type u} [Category.{v} C] (X : C) where
…
  30. instance OAI.PartitionConsistency.ConstructionIteration.(instance at line 252) line 252
  31. instance OAI.PartitionConsistency.ConstructionIteration.(instance at line 257) line 257
  32. instance OAI.PartitionConsistency.ConstructionIteration.(instance at line 258) line 258
  33. def OAI.PartitionConsistency.ConstructionIteration.structureWithTime line 262
  34. abbrev OAI.PartitionConsistency.ConstructionIteration.fullFunctor line 267
  35. abbrev OAI.PartitionConsistency.ConstructionIteration.functor line 268
  36. abbrev OAI.PartitionConsistency.ConstructionIteration.timeFunctor line 269
  37. theorem OAI.PartitionConsistency.ConstructionIteration.time line 271
  38. def OAI.PartitionConsistency.ConstructionIteration.botIso line 297
  39. def OAI.PartitionConsistency.ConstructionIteration.succIso line 300
  40. theorem OAI.PartitionConsistency.ConstructionIteration.map_succ line 305
  41. instance OAI.PartitionConsistency.MonoidConstruction.(instance at line 330) line 330