OAI/SetTheory/PartitionPrinciple/Transfinite/GroundTwoStageMainDiagram.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.OldBirthFiberCoverageCode line 11
  2. theorem OAI.PartitionPilot.Forcing.OldBirthFiberCoverageCode.fiber_entry_iff line 20
  3. theorem OAI.PartitionPilot.Forcing.OldBirthFiberCoverageCode.mono_cutoff line 32
  4. structure OAI.PartitionPilot.Forcing.GroundChronologicalMainStage line 44
  5. def OAI.PartitionPilot.Forcing.GroundChronologicalMainStage.birth line 59
  6. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainStage.birth_ground line 61
  7. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainStage.birth_function line 64
  8. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainStage.birth_bound line 68
  9. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainStage.old_meet line 74
  10. def OAI.PartitionPilot.Forcing.GroundChronologicalMainStage.ofHistory line 78
  11. structure OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition line 96
  12. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.prefix_bound line 116
  13. def OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.identity line 126
  14. def OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.comp line 136
  15. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.ext line 153
  16. def OAI.PartitionPilot.Forcing.ChronologyGraphPrefixCode line 169
  17. structure OAI.PartitionPilot.Forcing.ChronologicalTransitionLaws line 173
  18. def OAI.PartitionPilot.Forcing.BoundedFormula.graphCutoffEqualityFormula line 182
  19. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_graphCutoffEqualityFormula line 186
  20. def OAI.PartitionPilot.Forcing.BoundedFormula.chronologyGraphPrefixFormula line 199
  21. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_chronologyGraphPrefixFormula line 207
  22. def OAI.PartitionPilot.Forcing.BoundedFormula.chronologicalTransitionExtraFormula line 216
  23. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_chronologicalTransitionExtraFormula line 223
  24. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_chronologicalTransitionExtraFormula line 244
  25. def OAI.PartitionPilot.Forcing.BoundedFormula.oldBirthFiberCoverageFormula line 257
  26. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_oldBirthFiberCoverageFormula line 264
  27. def OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.CoversOldBirths line 291
  28. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.CoversOldBirths.fiber_entry_iff line 294
  29. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.identity_coversOldBirths line 305
  30. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.CoversOldBirths.comp line 311
  31. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.identity_comp line 334
  32. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.comp_identity line 340
  33. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.comp_assoc line 346
  34. structure OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram line 361
  35. def OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.CoversOldBirths line 380
  36. def OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.twoStageStage line 397
  37. def OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.twoStageTransition line 401
  38. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.twoStage_index_cases line 414
  39. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.twoStageTransition_self line 423
  40. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.twoStageTransition_comp line 428
  41. def OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.twoStage line 444
  42. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.twoStage_stage_zero line 450
  43. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.twoStage_stage_one line 452
  44. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.twoStage_transition_zero_one line 454
  45. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.twoStage_coversOldBirths line 457