OAI/SetTheory/PartitionPrinciple/Transfinite/StageOneDataBoundLaws.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.stageOneAssignment line 10
  2. def OAI.PartitionPilot.Forcing.stageOneAssignments line 13
  3. theorem OAI.PartitionPilot.Forcing.stageOneAssignment_eq_iff line 16
  4. theorem OAI.PartitionPilot.Forcing.stageOneAssignment_mem_assignments line 21
  5. theorem OAI.PartitionPilot.Forcing.mem_stageOneAssignments line 26
  6. def OAI.PartitionPilot.Forcing.stageOneAssignmentLevels line 37
  7. theorem OAI.PartitionPilot.Forcing.pair_mem_stageOneAssignmentLevels line 40
  8. theorem OAI.PartitionPilot.Forcing.stageOneAssignmentLevels_function line 45
  9. theorem OAI.PartitionPilot.Forcing.stageOneAssignmentCut_zero line 52
  10. theorem OAI.PartitionPilot.Forcing.stageOneAssignmentCut_one line 63
  11. def OAI.PartitionPilot.Forcing.BoundedFormula.stageOneAssignmentFormula line 73
  12. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_stageOneAssignmentFormula line 76
  13. def OAI.PartitionPilot.Forcing.TransitiveGround.groundSmallSubsets line 92
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_groundSmallSubsets line 95
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundSmallSubsets_mem line 100
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignment_mem line 118
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignment_fields_mem line 123
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignments_mem line 128
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignmentLevels_mem line 136
  20. def OAI.PartitionPilot.Forcing.TransitiveGround.stageOneCandidateBound line 148
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_stageOneCandidateBound line 151
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_stageOneCandidateBound line 157
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneCandidateBound_mem line 169
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneCandidateBound_empty line 179
  25. def OAI.PartitionPilot.Forcing.stageOneDataBounds line 193
  26. theorem OAI.PartitionPilot.Forcing.mem_stageOneDataBounds line 201
  27. theorem OAI.PartitionPilot.Forcing.pair_mem_stageOneDataBounds line 215
  28. def OAI.PartitionPilot.Forcing.BoundedFormula.stageOneDataBoundEntryFormula line 231
  29. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_stageOneDataBoundEntryFormula line 245
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneDataBounds_mem line 263
  31. theorem OAI.PartitionPilot.Forcing.stageOneDataBounds_assignment_entry line 296
  32. theorem OAI.PartitionPilot.Forcing.stageOneDataBounds_mono line 311
  33. theorem OAI.PartitionPilot.Forcing.stageOneDataBounds_total line 325