OAI/SetTheory/PartitionPrinciple/Forcing/GroundRenamedNameFamilyBounds.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PartitionPilot.Forcing.NiceNameSystem line 12
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceNormalize_mem_niceNameCandidates line 60
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceNormalize_mem_eval_niceVisibilityName line 70
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceNameSystem line 85
5. def OAI.PartitionPilot.Forcing.TransitiveGround.stageOneClassName line 131
6. def OAI.PartitionPilot.Forcing.TransitiveGround.stageOneMapName line 136
7. def OAI.PartitionPilot.Forcing.TransitiveGround.stageOneVisibilityName line 145
8. def OAI.PartitionPilot.Forcing.TransitiveGround.visibleSupportProfile line 162
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.encode_mem_visibleSupportProfile line 166
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.visibleSupportProfile_upward line 171
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.visibleSupportProfile_nonempty line 192
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.visibleSupportProfile_meet line 211
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.visibleSupportProfile_filter line 230
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairEmpty_name_mem line 261
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairEmpty_name_inverse_mem line 267
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairEmpty_name_ground_iff line 274
17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairEmpty_nameFamily line 291
18. theorem OAI.PartitionPilot.Forcing.Name.renamedFamily_inverse line 328
19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.renamedFamily_below line 352
20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairEmpty_renamedFamily_below line 370
21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairEmpty_niceNameSystem line 393