OAI/SetTheory/PartitionPrinciple/Transfinite/ExternalChronologyStageLaws.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.ownerLevelPrefix line 10
  2. theorem OAI.PartitionPilot.Forcing.mem_ownerLevelPrefix line 14
  3. theorem OAI.PartitionPilot.Forcing.ownerLevelPrefix_old line 19
  4. theorem OAI.PartitionPilot.Forcing.ownerLevelPrefix_subset line 22
  5. theorem OAI.PartitionPilot.Forcing.mem_ownerLevelPrefix_fresh line 27
  6. theorem OAI.PartitionPilot.Forcing.omegaMemberOrEqual_trans line 34
  7. theorem OAI.PartitionPilot.Forcing.ownerLevelPrefix_mono line 48
  8. theorem OAI.PartitionPilot.Forcing.ownerLevelPrefix_union line 57
  9. theorem OAI.PartitionPilot.Forcing.ownerLevelPrefix_lower line 73
  10. def OAI.PartitionPilot.Forcing.ownerLevelPrefixPoints line 96
  11. theorem OAI.PartitionPilot.Forcing.pair_mem_ownerLevelPrefixPoints line 100
  12. theorem OAI.PartitionPilot.Forcing.ownerLevelPrefixPoints_fiber line 111
  13. def OAI.PartitionPilot.Forcing.BoundedFormula.ownerLevelPrefixFormula line 122
  14. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_ownerLevelPrefixFormula line 127
  15. def OAI.PartitionPilot.Forcing.BoundedFormula.ownerLevelPrefixPointFormula line 135
  16. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_ownerLevelPrefixPointFormula line 139
  17. def OAI.PartitionPilot.Forcing.TransitiveGround.ownerLevelPrefixFamily line 156
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ownerLevelPrefixPoints_mem line 166
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ownerLevelPrefix_mem line 182
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ownerLevelPrefixFamily_spec line 188
  21. theorem OAI.PartitionPilot.Forcing.PartialOrderCode.heightOrderRestriction line 209
  22. theorem OAI.PartitionPilot.Forcing.MeetOrderCode.restrict_lower line 221
  23. theorem OAI.PartitionPilot.Forcing.StrictLexHeightCode.restrict_order line 253
  24. theorem OAI.PartitionPilot.Forcing.ownerLevelPrefix_codes line 265
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.heightOrderRestriction_mem line 286
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ownerLevelPrefix_fields_mem line 292
  27. def OAI.PartitionPilot.Forcing.chronologyRestriction line 312
  28. def OAI.PartitionPilot.Forcing.BoundedFormula.chronologyRestrictionMemberFormula line 318
  29. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_chronologyRestrictionMemberFormula line 323
  30. def OAI.PartitionPilot.Forcing.BoundedFormula.chronologyRestrictionFormula line 345
  31. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_chronologyRestrictionFormula line 349
  32. def OAI.PartitionPilot.Forcing.BoundedFormula.chronologyRestrictionFamilyFormula line 377
  33. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_chronologyRestrictionFamilyFormula line 384
  34. def OAI.PartitionPilot.Forcing.TransitiveGround.chronologyRestrictionFamily line 401
  35. theorem OAI.PartitionPilot.Forcing.TransitiveGround.chronologyRestriction_mem line 411
  36. theorem OAI.PartitionPilot.Forcing.TransitiveGround.chronologyRestrictionFamily_mem line 418
  37. theorem OAI.PartitionPilot.Forcing.TransitiveGround.chronologyRestrictionFamily_entries line 440
  38. theorem OAI.PartitionPilot.Forcing.TransitiveGround.chronologyRestrictionFamily_function line 463
  39. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff line 490
  40. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoffFamily line 493
  41. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoffOrder line 497
  42. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoffMeet line 498
  43. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoffBirth line 499
  44. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoffHeight line 500
  45. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff_old line 502
  46. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff_subset line 504
  47. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff_mono line 507
  48. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff_union line 513
  49. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff_birth_function line 518
  50. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff_old_meet line 525
  51. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff_birth_bound line 533
  52. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoffFamily_spec line 561
  53. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff_lower line 570
  54. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff_fields line 585
  55. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff_iff_birth_le_stamp line 626
  56. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.point_in_birth_cutoff line 652
  57. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.fresh_birth_cutoff_iff line 656
  58. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronologyFields line 686
  59. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronologyFields_old line 696
  60. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronologyFields_stamp line 707
  61. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronologyFields_limit line 718
  62. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronologyFields_stage_laws line 745