OAI/SetTheory/PartitionPrinciple/Geometry/MainDiagrams.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.stage line 12
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.step line 16
  3. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.transition line 19
  4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.transition_self line 22
  5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.transition_step line 25
  6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.points_comp line 29
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.actors_comp line 41
  8. abbrev OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.Index line 53
  9. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.orders line 55
  10. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.groups line 69
  11. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.actions line 83
  12. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.heights line 87
  13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.agreements line 92
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.step_strict_top line 95
  15. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.omegaHeight line 109
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.omegaHeight_stage line 115
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.omegaHeight_countable line 119
  18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.union_bottom_at line 122
  19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.union_bottom_least line 130
  20. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.omega line 137
  21. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.omegaTransition line 152
  22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.omega_points_coherent line 161
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.omega_actors_coherent line 166
  24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.omega_strict_top line 171
  25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.omega_point_cover line 175
  26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.omega_actor_cover line 183
  27. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.countableOrdinalLabelsOmega line 188
  28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.ext line 200
  29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.identity_comp line 217
  30. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.comp_identity line 220
  31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.comp_assoc line 223
  32. structure OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram line 229
  33. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.reindex line 239
  34. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.constant line 245
  35. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.orders line 251
  36. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.groups line 265
  37. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.actions line 279
  38. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.heights line 283
  39. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.agreements line 288
  40. structure OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Cone line 291
  41. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Cone.extend line 296
  42. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Diagram.Cone.reindex line 301
  43. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.FiniteRun.diagram line 309