OAI/SetTheory/PartitionPrinciple/Geometry/GroundRefinementRawTestMonotonicity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelTests line 25
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelTests_zero line 40
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelTests_mono line 46
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelTests_subset line 63
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelTests_empty line 76
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelTests_transfer line 85
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelTests_congr line 103
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelTests_of_no_assignments line 120
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelTests_stageTwoSplice line 137
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelTests_stageTwoOld line 149
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelTests_union line 176
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelTests_stageTwoUnion line 224
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelRawSingle_iff line 258
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelRawTests_iff line 286
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelRawTests_mono line 321
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementLevelRawTests_order_mono line 330