OAI/SetTheory/PartitionPrinciple/Transfinite/CompressionPrefixCoinitiality.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.GroundCompressionState.incoming_birth_layer_of_constancy line 18
  2. def OAI.PartitionPilot.Forcing.GroundCompressionState.canonical_incoming_birth_layer line 46
  3. def OAI.PartitionPilot.Forcing.GroundCompressionState.ground_birth_incoming_layer line 108
  4. def OAI.PartitionPilot.Forcing.GroundCompressionState.ground_birth_prior_layer line 121
  5. def OAI.PartitionPilot.Forcing.GroundCompressionState.ground_birth_limit_layer line 129
  6. def OAI.PartitionPilot.Forcing.GroundCompressionState.canonical_birth_layer_to_finite line 160
  7. def OAI.PartitionPilot.Forcing.GroundCompressionState.prior_birth_layer_to_finite line 187
  8. def OAI.PartitionPilot.Forcing.GroundCompressionState.ground_birth_finite_all_layers line 205
  9. def OAI.PartitionPilot.Forcing.GroundCompressionState.ground_birth_all_layers line 257
  10. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.prefix_sources_eq_below line 300
  11. def OAI.PartitionPilot.Forcing.GroundCompressionState.prefix_old_layer line 312
  12. def OAI.PartitionPilot.Forcing.GroundCompressionState.prefix_base_layers line 340
  13. def OAI.PartitionPilot.Forcing.GroundCompressionState.prefix_finite_layers line 357
  14. def OAI.PartitionPilot.Forcing.GroundCompressionState.prefix_union_layers line 371
  15. def OAI.PartitionPilot.Forcing.GroundCompressionState.prefix_all_layers line 385
  16. def OAI.PartitionPilot.Forcing.GroundCompressionState.prefixHistory line 431
  17. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.prefixHistory_old line 466
  18. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.prefixHistory_stamp line 472
  19. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.prefixHistory_limit line 481
  20. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.prefix_exists_extension_basis line 520