OAI/SetTheory/PartitionPrinciple/Transfinite/OrdinalExternalHeights.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.Column line 15
  2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.membership_iff line 17
  3. def OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.order line 21
  4. def OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.add line 31
  5. def OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.natural line 34
  6. def OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.omega line 37
  7. def OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.start line 39
  8. def OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.layer line 40
  9. def OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.cap line 41
  10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.layer_increasing line 43
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.starts_above line 48
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.below_cap line 53
  13. def OAI.PartitionPilot.Compression.RecursiveMaps.CountableColumns.room line 56
  14. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.ordinalExtensionHeight line 73
  15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.ordinalExtensionHeight_original line 77
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.ordinalExtensionHeight_countable line 82
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.ordinalExtensionHeight_top line 86
  18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.ordinal_external_height_extension line 91