OAI/SetTheory/PartitionPrinciple/Geometry/DecodedMeetMaps.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.MeetEmbeddingCode.value line 16
2. theorem OAI.PartitionPilot.Forcing.MeetEmbeddingCode.value_entry line 22
3. theorem OAI.PartitionPilot.Forcing.MeetEmbeddingCode.value_eq_iff line 26
4. def OAI.PartitionPilot.Forcing.MeetEmbeddingCode.toMeetEmbedding line 36
5. theorem OAI.PartitionPilot.Forcing.MeetEmbeddingCode.toMeetEmbedding_entry line 51
6. theorem OAI.PartitionPilot.Forcing.MeetEmbeddingCode.toMeetEmbedding_eq_iff line 56
7. def OAI.PartitionPilot.Forcing.PosetActionCode.rawAct line 69
8. theorem OAI.PartitionPilot.Forcing.PosetActionCode.rawAct_entry line 78
9. theorem OAI.PartitionPilot.Forcing.PosetActionCode.rawAct_eq_iff line 84
10. theorem OAI.PartitionPilot.Forcing.PosetActionCode.rawAct_injective line 94
11. theorem OAI.PartitionPilot.Forcing.PosetActionCode.rawAct_surjective line 109
12. def OAI.PartitionPilot.Forcing.PosetActionCode.toMeetIso line 115
13. theorem OAI.PartitionPilot.Forcing.PosetActionCode.toMeetIso_entry line 133
14. theorem OAI.PartitionPilot.Forcing.PosetActionCode.toMeetIso_eq_iff line 138