OAI/SetTheory/PartitionPrinciple/Geometry/RowPositionBounds.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.RowPositionSequenceAt line 10
2. def OAI.PartitionPilot.Forcing.RowPositionSequenceCode line 13
3. theorem OAI.PartitionPilot.Forcing.rowPositionSequence_length line 16
4. theorem OAI.PartitionPilot.Forcing.RowPositionSequenceCode.shape line 23
5. theorem OAI.PartitionPilot.Forcing.RowPositionSequenceAt.domain_unique line 31
6. def OAI.PartitionPilot.Forcing.BoundedFormula.rowPositionSequenceAtFormula line 46
7. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_rowPositionSequenceAtFormula line 52
8. def OAI.PartitionPilot.Forcing.BoundedFormula.rowPositionSequenceFormula line 70
9. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_rowPositionSequenceFormula line 74
10. def OAI.PartitionPilot.Forcing.TransitiveGround.rowPositionSequences line 95
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_rowPositionSequences line 98
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowPositionSequences_mem line 104
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowPositionSequence_data line 124
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.empty_mem_rowPositionSequences line 138
15. def OAI.PartitionPilot.Forcing.RowPositionBound line 161
16. def OAI.PartitionPilot.Forcing.BoundedFormula.rowPositionBoundFormula line 166
17. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_rowPositionBoundFormula line 171
18. theorem OAI.PartitionPilot.Forcing.RowPositionBound.mono line 188
19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowPositionSequence_bound line 202