OAI/SetTheory/PartitionPrinciple/Transfinite/NonzeroLimitOrdinalCodes.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PartitionPilot.Forcing.MainTransitionIndex line 9
  2. def OAI.PartitionPilot.Forcing.mainTransitionIndexKey line 11
  3. theorem OAI.PartitionPilot.Forcing.mainTransitionIndexKey_injective line 14
  4. theorem OAI.PartitionPilot.Forcing.mainTransitionIndex_range line 21
  5. def OAI.PartitionPilot.Forcing.finiteMainIndexKey line 39
  6. theorem OAI.PartitionPilot.Forcing.finiteMainIndexKey_injective line 41
  7. theorem OAI.PartitionPilot.Forcing.finiteMainIndexKey_order line 45
  8. theorem OAI.PartitionPilot.Forcing.finiteMainIndexKey_range line 51
  9. theorem OAI.PartitionPilot.Forcing.finiteMainTransitionIndex_range line 59
  10. def OAI.PartitionPilot.Forcing.ordinalMainIndexPreorder line 73
  11. theorem OAI.PartitionPilot.Forcing.ordinalMainIndex_le_iff line 85
  12. theorem OAI.PartitionPilot.Forcing.ordinalMainIndex_key_range line 90
  13. theorem OAI.PartitionPilot.Forcing.ordinalMainTransitionIndex_range line 101
  14. theorem OAI.PartitionPilot.Forcing.ordinalMainIndex_rank_le_iff line 109
  15. theorem OAI.PartitionPilot.Forcing.ordinalMainIndex_total line 126
  16. theorem OAI.PartitionPilot.Forcing.ordinalMainIndex_antisymm line 135
  17. theorem OAI.PartitionPilot.Forcing.ordinalMainIndex_common_upper line 149
  18. def OAI.PartitionPilot.Forcing.NonzeroLimitOrdinalCode line 158
  19. theorem OAI.PartitionPilot.Forcing.not_nonzeroLimitOrdinalCode_successor line 161
  20. theorem OAI.PartitionPilot.Forcing.ordinal_successor_or_nonzeroLimit line 171
  21. theorem OAI.PartitionPilot.Forcing.nonzeroLimitOrdinalCode_iff_not_successor line 197