OAI/SetTheory/PartitionPrinciple/Geometry/LiftedCompressionFunctions.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.liftOldEntry line 11
2. def OAI.PartitionPilot.Forcing.liftFreshEntry line 14
3. def OAI.PartitionPilot.Forcing.liftedCompressionGraph line 21
4. theorem OAI.PartitionPilot.Forcing.pair_mem_liftedCompressionGraph line 27
5. theorem OAI.PartitionPilot.Forcing.liftFreshEntry_not_old line 41
6. theorem OAI.PartitionPilot.Forcing.liftOldEntry_iff line 47
7. theorem OAI.PartitionPilot.Forcing.liftedCompressionGraph_old_iff line 56
8. theorem OAI.PartitionPilot.Forcing.liftFreshEntry_iff line 68
9. theorem OAI.PartitionPilot.Forcing.liftedCompressionGraph_fresh_iff line 87
10. theorem OAI.PartitionPilot.Forcing.liftedCompressionGraph_function line 107
11. theorem OAI.PartitionPilot.Forcing.indexedRelationSection_function line 159
12. theorem OAI.PartitionPilot.Forcing.liftedCompressionSection_function line 170