OAI/SetTheory/PartitionPrinciple/Transfinite/ExternalBirthLayerSeparation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerFiber line 23
  2. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerOwners line 24
  3. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerComponents line 25
  4. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerIndices line 26
  5. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerMaps line 27
  6. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerWitness line 29
  7. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.mem_layerFiber line 33
  8. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerFiber_level line 37
  9. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerOwners_cases line 41
  10. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.layer_fields_ground line 54
  11. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerComponents_function line 72
  12. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerIndices_function line 84
  13. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerMaps_spec line 91
  14. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerWitness_ground line 99
  15. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerMaps_copy line 134
  16. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerMaps_embedding line 165
  17. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerMaps_outputs_cutoff line 178
  18. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerMaps_cutoff_embedding line 196
  19. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerFiber_cutoff line 233
  20. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.layerComponents_earlier_meet line 252