OAI/SetTheory/PartitionPrinciple/Forcing/GroundBatchEarlierLayerWitnesses.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.CountableLayerCode.of_literal_extension line 11
  2. theorem OAI.PartitionPilot.Forcing.CopyLayerCode.of_literal_extension line 18
  3. theorem OAI.PartitionPilot.Forcing.SeparatedLayerCode.of_literal_extension line 38
  4. theorem OAI.PartitionPilot.Forcing.GrowthLayerWitnessCode.exists_literal_extension line 63
  5. theorem OAI.PartitionPilot.Forcing.GrowthLayerWitnessCode.exists_fixedTop_earlier line 89
  6. def OAI.PartitionPilot.Forcing.fixedTopLayerWitness line 105
  7. theorem OAI.PartitionPilot.Forcing.fixedTopLayerWitness_code line 108
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fixedTopLayerWitness_mem line 116
  9. theorem OAI.PartitionPilot.Forcing.GrowthLayerWitnessCode.exists_literal_extension_rank_lt line 130
  10. theorem OAI.PartitionPilot.Forcing.GrowthLayerWitnessCode.exists_fixedTop_earlier_rank_lt line 168
  11. theorem OAI.PartitionPilot.Forcing.fixedTopLayerWitness_rank_lt line 186
  12. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.exists_batchEarlierLayerWitness line 202
  13. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_birthWitness_to_finite_rank_lt line 244
  14. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_birthWitness_to_union_rank_lt line 269
  15. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_priorWitness_to_finite_rank_lt line 289
  16. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_priorWitness_to_union_rank_lt line 300
  17. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_limitWitness_rank_lt line 309
  18. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_birthWitness_to_finite line 337
  19. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_birthWitness_to_union line 362
  20. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_priorWitness_to_finite line 382
  21. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_priorWitness_to_union line 393
  22. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_limitWitness line 402