OAI/SetTheory/PartitionPrinciple/Transfinite/GroundInvariantSuccessors.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_old_iff line 15
  2. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_image_base_iff line 25
  3. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_cut_iff line 33
  4. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_range_below_cap line 54
  5. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_fresh_outside_base line 68
  6. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.negative_cap_persists line 83
  7. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_cap_and_source_unchanged line 93
  8. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.liftSection_negative_exclusion line 102
  9. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.original_carrier_subset line 141
  10. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.original_order_iff line 144
  11. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.original_meet_iff line 150
  12. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextAction_original_iff line 166
  13. structure OAI.PartitionPilot.Forcing.RecursiveCompressionInvariant line 181
  14. theorem OAI.PartitionPilot.Forcing.RecursiveCompressionInvariant.compatible line 212
  15. theorem OAI.PartitionPilot.Forcing.CodedRecursiveTaskAction.exists_groundSuccessor line 246
  16. theorem OAI.PartitionPilot.Forcing.RecursiveCompressionInvariant.nextAgreement line 296
  17. theorem OAI.PartitionPilot.Forcing.RecursiveCompressionInvariant.nextNegative line 313
  18. theorem OAI.PartitionPilot.Forcing.RecursiveCompressionInvariant.nextInvariant line 338
  19. structure OAI.PartitionPilot.Forcing.RecursiveGroundFields line 360
  20. theorem OAI.PartitionPilot.Forcing.RecursiveGroundFields.current_codes line 389
  21. theorem OAI.PartitionPilot.Forcing.RecursiveGroundFields.next_fields line 396
  22. theorem OAI.PartitionPilot.Forcing.RecursiveGroundFields.next_codes line 423
  23. theorem OAI.PartitionPilot.Forcing.RecursiveGroundFields.next line 433
  24. theorem OAI.PartitionPilot.Forcing.RecursiveCompressionInvariant.exists_groundNext line 468