OAI/SetTheory/PartitionPrinciple/Transfinite/GroundBatchBirths.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.NatUnionCode.oldMeet line 11
  2. theorem OAI.PartitionPilot.Forcing.NatUnionCode.birth_bound line 31
  3. theorem OAI.PartitionPilot.Forcing.NatUnionCode.no_birth_at_bound line 39
  4. theorem OAI.PartitionPilot.Forcing.NatUnionCode.stable_birth_entry_iff line 46
  5. theorem OAI.PartitionPilot.Forcing.NatUnionCode.stable_birth_fiber line 56
  6. theorem OAI.PartitionPilot.Forcing.MeetEmbeddingCode.enlarge_target line 70
  7. theorem OAI.PartitionPilot.Forcing.relationImage_enlarge_target line 83
  8. theorem OAI.PartitionPilot.Forcing.OldBridgeCode.of_literal_extension line 89
  9. def OAI.PartitionPilot.Forcing.CodedGrowthLayer.of_literal_extension line 100
  10. def OAI.PartitionPilot.Forcing.fixedTopBirth line 137
  11. theorem OAI.PartitionPilot.Forcing.pair_mem_fixedTopBirth line 140
  12. theorem OAI.PartitionPilot.Forcing.fixedTopBirth_subset line 145
  13. theorem OAI.PartitionPilot.Forcing.fixedTopBirth_old_iff line 148
  14. theorem OAI.PartitionPilot.Forcing.fixedTopBirth_top_iff line 154
  15. theorem OAI.PartitionPilot.Forcing.fixedTopBirth_function line 161
  16. theorem OAI.PartitionPilot.Forcing.fixedTopBirth_bound line 177
  17. theorem OAI.PartitionPilot.Forcing.fixedTopBirth_new_time_iff line 184
  18. theorem OAI.PartitionPilot.Forcing.fixedTopBirth_earlier_iff line 191
  19. theorem OAI.PartitionPilot.Forcing.fixedTopBirth_oldMeet line 197
  20. theorem OAI.PartitionPilot.Forcing.fixedTopBirth_singleton_injection line 223
  21. def OAI.PartitionPilot.Forcing.CodedGrowthLayer.of_natUnion line 246
  22. def OAI.PartitionPilot.Forcing.CodedGrowthLayer.empty_of_no_birth line 261
  23. def OAI.PartitionPilot.Forcing.CodedGrowthLayer.empty_at_birth_bound line 269
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fixedTopBirth_mem line 284
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fixedTopBirth_singleton_small line 291
  26. def OAI.PartitionPilot.Forcing.TransitiveGround.fixedTopBirth_incoming_layer line 302
  27. def OAI.PartitionPilot.Forcing.TransitiveGround.fixedTopBirth_earlier_layer line 313
  28. def OAI.PartitionPilot.Forcing.TransitiveGround.fixedTopBirth_layers line 328
  29. abbrev OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchBirth line 353
  30. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchBirth_function line 356
  31. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchBirth_fresh_entry_iff line 360
  32. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchBirth_oldMeet line 365
  33. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchBirth_fresh_cases line 397
  34. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchBirth_different_components_bridge line 407
  35. theorem OAI.PartitionPilot.Forcing.TransitiveGround.taggedBirth_mem line 441
  36. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchBirth_mem line 462
  37. def OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchBirth_earlier_layer line 472
  38. def OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchBirth_incoming_layer line 494