OAI/SetTheory/PartitionPrinciple/Transfinite/GroundCountableProducts.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.relationProduct line 11
2. theorem OAI.PartitionPilot.Forcing.mem_relationProduct line 17
3. theorem OAI.PartitionPilot.Forcing.pair_mem_relationProduct line 29
4. theorem OAI.PartitionPilot.Forcing.relationProduct_function line 42
5. theorem OAI.PartitionPilot.Forcing.relationProduct_injection line 59
6. def OAI.PartitionPilot.Forcing.BoundedFormula.relationProductEntryFormula line 75
7. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_relationProductEntryFormula line 81
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.relationProduct_mem line 98
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.countableProduct_injection line 122
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEmbeddable_product line 141