OAI/SetTheory/PartitionPrinciple/Definability/GroundDefinableRelationProducts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.GroundDefinableFunction.congr line 13
2. structure OAI.PartitionPilot.Forcing.GroundSetTerm line 24
3. def OAI.PartitionPilot.Forcing.GroundSetTerm.var line 30
4. def OAI.PartitionPilot.Forcing.GroundSetTerm.app line 33
5. theorem OAI.PartitionPilot.Forcing.GroundSetTerm.ground line 40
6. theorem OAI.PartitionPilot.Forcing.GroundSetTerm.correct line 44
7. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_nonemptyTuple line 53
8. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_relationProduct line 78