OAI/SetTheory/PartitionPrinciple/Forcing/GroundCompressionIncomingWitnessRanks.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleBatchLayerWitness line 13
2. theorem OAI.PartitionPilot.Forcing.batchFamilyPointBound_rank_le line 49
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.batchTemplateFamilyBound_rank_lt line 58
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.batchTemplateFamily_rank_lt line 67
5. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchIncomingFiber_rank_lt line 88
6. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.constantBatchLayerWitness_rank_lt line 96
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleBatchLayerWitness_rank_lt line 116
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleBatchLayerWitness_ranked line 127
9. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_canonicalIncomingRankedWitness line 167