OAI/SetTheory/PartitionPrinciple/Geometry/LiftedCompressionEmbeddings.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftGraph_entry line 13
2. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftGraph_entry_iff line 33
3. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_entry line 44
4. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_entry_iff line 51
5. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_order_iff line 62
6. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_injection line 75
7. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_map_meet line 89
8. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_embedding line 113