OAI/SetTheory/PartitionPrinciple/Transfinite/LinkedSuccessorOutputFieldEquality.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_0 line 8
  2. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_1 line 12
  3. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_2 line 16
  4. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_3 line 20
  5. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_4 line 24
  6. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_5 line 28
  7. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_6 line 32
  8. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_7 line 36
  9. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_8 line 40
  10. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_9 line 44
  11. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_10 line 48
  12. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_11 line 52
  13. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_12 line 56
  14. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_13 line 60
  15. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_14 line 64
  16. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_15 line 68
  17. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_16 line 72
  18. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_17 line 76
  19. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_18 line 80
  20. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_19 line 84
  21. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_20 line 88
  22. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_21 line 92
  23. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_22 line 96
  24. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_23 line 100
  25. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_24 line 104
  26. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_25 line 108
  27. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_26 line 112
  28. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_27 line 116
  29. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_28 line 120
  30. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_29 line 124
  31. theorem OAI.PartitionPilot.Forcing.linkedSuccessorOutputFields_eq line 128