OAI/SetTheory/PartitionPrinciple/Definability/ExternalStarCarrierRanks.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupCarrier_rank_lt line 17
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalRequestWords_rank_lt line 24
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalRequestGroup_rank_lt line 30
4. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalPointCarrier_rank_lt line 47
5. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalPointCarrier_rank_lt_of_inputs line 55
6. theorem OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalBoundedCarrier_rank_lt line 63
7. theorem OAI.PartitionPilot.Forcing.taggedSumCarrier_rank_lt line 82
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalStarVertices_rank_lt line 93
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalStarVertices_rank_lt_of_inputs line 101