OAI/SetTheory/PartitionPrinciple/Models/GroundCountableQuotients.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PartitionPilot.Forcing.EquivalenceRelationCode line 9
2. def OAI.PartitionPilot.Forcing.canonicalRepresentativeProperty line 15
3. def OAI.PartitionPilot.Forcing.canonicalRepresentatives line 19
4. theorem OAI.PartitionPilot.Forcing.mem_canonicalRepresentatives line 22
5. theorem OAI.PartitionPilot.Forcing.canonicalRepresentatives_subset line 26
6. theorem OAI.PartitionPilot.Forcing.canonical_exists line 30
7. theorem OAI.PartitionPilot.Forcing.canonical_equiv_eq line 48
8. theorem OAI.PartitionPilot.Forcing.canonical_exists_unique line 64
9. def OAI.PartitionPilot.Forcing.canonicalRepresentativesInjection line 73
10. theorem OAI.PartitionPilot.Forcing.canonicalRepresentativesInjection_code line 76
11. def OAI.PartitionPilot.Forcing.BoundedFormula.canonicalRepresentativeFormula line 85
12. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_canonicalRepresentativeFormula line 90
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.canonicalRepresentatives_mem line 105
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.canonicalRepresentativesInjection_mem line 121
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.canonicalRepresentatives_spec line 127