OAI/SetTheory/PartitionPrinciple/Geometry/GroundDefinableRowAssignmentOrders.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.rawRowAssignmentOrder line 10
2. theorem OAI.PartitionPilot.Forcing.pair_mem_rawRowAssignmentOrder line 13
3. theorem OAI.PartitionPilot.Forcing.rawRowAssignmentOrder_eq line 24
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryOrder_raw line 42
5. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_rowAssignmentOrder line 60
6. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_rawRowAssignmentOrder line 94
7. def OAI.PartitionPilot.Forcing.TransitiveGround.rawRowAssignmentOrderOutputFormula line 101
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_rawRowAssignmentOrderOutputFormula line 106