OAI/SetTheory/PartitionPrinciple/Definability/SetPresentations.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PartitionPilot.SetRealization.Presentation line 13
2. theorem OAI.PartitionPilot.SetRealization.Presentation.encode_mem line 22
3. def OAI.PartitionPilot.SetRealization.Presentation.carrierEquiv line 25
4. def OAI.PartitionPilot.SetRealization.Presentation.ordinalIndex line 32
5. def OAI.PartitionPilot.SetRealization.Presentation.canonical line 36
6. theorem OAI.PartitionPilot.SetRealization.Presentation.rank_canonical line 51
7. theorem OAI.PartitionPilot.SetRealization.Presentation.canonical_rank_lt line 54
8. def OAI.PartitionPilot.SetRealization.Presentation.product line 59
9. def OAI.PartitionPilot.SetRealization.Presentation.subset line 76
10. theorem OAI.PartitionPilot.SetRealization.Presentation.mem_subset line 79
11. theorem OAI.PartitionPilot.SetRealization.Presentation.encode_mem_subset line 88
12. theorem OAI.PartitionPilot.SetRealization.Presentation.subset_carrier line 97
13. theorem OAI.PartitionPilot.SetRealization.Presentation.rank_subset_le line 102