OAI/SetTheory/PartitionPrinciple/Transfinite/MainBirthOrigins.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealEmbedding.preserves_bottom line 14
  2. structure OAI.PartitionPilot.Compression.RecursiveMaps.MainStage line 22
  3. structure OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition line 39
  4. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.identity line 55
  5. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.Transition.comp line 64
  6. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.tasks line 92
  7. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.internal line 95
  8. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.internalTransition line 111
  9. inductive OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.RequestIndex line 121
  10. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.request line 126
  11. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.requests line 133
  12. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.next line 138
  13. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.externalTransition line 153
  14. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.nextTransition line 170
  15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.next_strict_top line 173
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.compression_requested line 178
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.separation_requested line 182
  18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.rectangle_requested line 186
  19. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.internalBirth line 202
  20. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.nextBirth line 205
  21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.nextBirth_original line 209
  22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.nextBirth_top line 219
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.nextBirth_cases line 222
  24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.internalBirth_before_external line 241
  25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.nextBirth_le line 251
  26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.nextBirth_old_meet line 262
  27. abbrev OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.Index line 291
  28. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.main line 293
  29. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.inside line 294
  30. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.outside line 295
  31. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.top line 296
  32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.main_inside line 298
  33. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.main_outside line 299
  34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.main_top line 300
  35. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.top_before line 302
  36. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.inside_before line 305
  37. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.outside_top line 309
  38. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.inside_increasing line 313
  39. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.outside_increasing line 317
  40. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.top_mono line 321
  41. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.BirthLabels.main_le line 326
  42. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.stageBirth_source line 339
  43. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.unionBirth_source line 361
  44. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.externalBirth_source line 375
  45. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.nextBirth_source line 388