OAI/SetTheory/PartitionPrinciple/Definability/TaggedExtensionCodes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.taggedExtension line 11
2. theorem OAI.PartitionPilot.Forcing.pair_tag_not_mem line 14
3. theorem OAI.PartitionPilot.Forcing.mem_taggedExtension line 23
4. theorem OAI.PartitionPilot.Forcing.old_mem_taggedExtension line 37
5. theorem OAI.PartitionPilot.Forcing.pair_mem_taggedExtension line 41
6. theorem OAI.PartitionPilot.Forcing.taggedExtension_disjoint line 51
7. def OAI.PartitionPilot.Forcing.taggedExtensionEncode line 58
8. theorem OAI.PartitionPilot.Forcing.taggedExtensionEncode_inl line 63
9. theorem OAI.PartitionPilot.Forcing.taggedExtensionEncode_inr line 66
10. theorem OAI.PartitionPilot.Forcing.taggedExtensionEncode_mem line 69
11. theorem OAI.PartitionPilot.Forcing.taggedExtensionEncode_injective line 76
12. theorem OAI.PartitionPilot.Forcing.taggedExtensionEncode_surjective line 93
13. def OAI.PartitionPilot.Forcing.taggedExtensionEquiv line 102