OAI/SetTheory/PartitionPrinciple/Transfinite/GroundCompressionBirthData.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.firstAppearanceBirth line 12
2. theorem OAI.PartitionPilot.Forcing.firstAppearanceBirth_subset line 17
3. theorem OAI.PartitionPilot.Forcing.pair_mem_firstAppearanceBirth line 21
4. theorem OAI.PartitionPilot.Forcing.firstAppearanceBirth_nat_iff line 36
5. theorem OAI.PartitionPilot.Forcing.firstAppearanceBirth_natValue_iff line 60
6. theorem OAI.PartitionPilot.Forcing.firstAppearanceBirth_old_subset line 69
7. def OAI.PartitionPilot.Forcing.BoundedFormula.firstAppearanceBirthEntryFormula line 84
8. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_firstAppearanceBirthEntryFormula line 97
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.firstAppearanceBirth_mem line 113
10. structure OAI.PartitionPilot.Forcing.NatBirthExtensionCode line 163
11. theorem OAI.PartitionPilot.Forcing.NatBirthExtensionCode.first_appearance_unique line 171
12. theorem OAI.PartitionPilot.Forcing.NatBirthExtensionCode.first_appearance_exists line 179
13. theorem OAI.PartitionPilot.Forcing.NatBirthExtensionCode.function line 192
14. theorem OAI.PartitionPilot.Forcing.NatBirthExtensionCode.old_entry_iff line 219
15. theorem OAI.PartitionPilot.Forcing.NatBirthExtensionCode.restriction_zero line 229
16. theorem OAI.PartitionPilot.Forcing.NatBirthExtensionCode.restriction_function line 241
17. theorem OAI.PartitionPilot.Forcing.NatBirthExtensionCode.restriction_union line 255
18. theorem OAI.PartitionPilot.Forcing.firstAppearanceBirth_code line 281
19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundFirstAppearanceBirth line 308
20. theorem OAI.PartitionPilot.Forcing.NatBirthExtensionCode.restriction_mono line 343
21. theorem OAI.PartitionPilot.Forcing.NatBirthExtensionCode.restriction_step line 350
22. theorem OAI.PartitionPilot.Forcing.NatBirthExtensionCode.restriction_bound line 383
23. theorem OAI.PartitionPilot.Forcing.NatBirthExtensionCode.earlier_fiber line 394
24. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.canonical_birth_function line 432
25. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.canonical_birth_step line 440
26. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.canonical_birth_before_stamp line 450
27. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.canonical_birth_oldMeet line 462
28. def OAI.PartitionPilot.Forcing.GroundCompressionState.canonical_birth_layer_to_union line 520
29. def OAI.PartitionPilot.Forcing.GroundCompressionState.prior_birth_layer_to_union line 543
30. def OAI.PartitionPilot.Forcing.GroundCompressionState.limit_birth_layer_empty line 556
31. structure OAI.PartitionPilot.Forcing.GroundCompressionBirthData line 572