OAI/SetTheory/PartitionPrinciple/Transfinite/GroundCountableRelationSelections.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.binaryUnionEnumeration line 12
2. theorem OAI.PartitionPilot.Forcing.pair_mem_binaryUnionEnumeration line 16
3. theorem OAI.PartitionPilot.Forcing.binaryUnionEnumeration_isFunc line 23
4. theorem OAI.PartitionPilot.Forcing.binaryUnionEnumeration_onto line 46
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.binaryUnionEnumeration_mem line 64
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundCountable_binary_union line 81
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.countablePartialFunctions_union line 101
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.countableFunction_common_extension line 118
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_countableRelationSelection line 159
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_countableNodeSelection line 170