OAI/SetTheory/PartitionPrinciple/Definability/GroundFunctionRangeFamilies.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.familyCodeGraph_eq_of_entries line 13
2. theorem OAI.PartitionPilot.Forcing.familyCodeGraph_ground_of_entries line 31
3. def OAI.PartitionPilot.Forcing.decodedFamilyValue line 38
4. theorem OAI.PartitionPilot.Forcing.decodedFamilyValue_entry line 42
5. theorem OAI.PartitionPilot.Forcing.decodedFamilyValue_eq line 46
6. theorem OAI.PartitionPilot.Forcing.decodedFamilyValue_ground line 51
7. theorem OAI.PartitionPilot.Forcing.decodedFamilyCodeGraph_eq line 56
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.familyCodeGraph_pair_projections line 74
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.familyCodeGraph_tuple_fields line 120
10. theorem OAI.PartitionPilot.Forcing.familyCodeGraph_rank_mono line 136
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.familyCodeGraph_functionRanges_ground line 157
12. theorem OAI.PartitionPilot.Forcing.familyCodeGraph_functionRanges_rank_le line 229