OAI/SetTheory/PartitionPrinciple/Transfinite/GroundStageOneAssignmentUnions.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BoundedFormula.refinementActivityFormula line 11
  2. def OAI.PartitionPilot.Forcing.BoundedFormula.refinementCollisionFormula line 14
  3. def OAI.PartitionPilot.Forcing.BoundedFormula.refinementProfileFormula line 17
  4. def OAI.PartitionPilot.Forcing.BoundedFormula.refinementCompatibilityFormula line 20
  5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_refinementActivityFormula line 23
  6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_refinementCollisionFormula line 26
  7. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_refinementProfileFormula line 31
  8. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_refinementCompatibilityFormula line 36
  9. def OAI.PartitionPilot.Forcing.SetFormula.refinementActivityFormula line 45
  10. def OAI.PartitionPilot.Forcing.SetFormula.refinementCollisionFormula line 47
  11. def OAI.PartitionPilot.Forcing.SetFormula.refinementProfileFormula line 49
  12. def OAI.PartitionPilot.Forcing.SetFormula.refinementCompatibilityFormula line 51
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementActivityFormula line 58
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementCollisionFormula line 64
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementProfileFormula line 70
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementCompatibilityFormula line 76
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementTest_forcing_mono line 91
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementActivity_eval line 97
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementCollision_eval line 109
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementProfile_eval line 121
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementCompatibility_eval line 133
  22. def OAI.PartitionPilot.Forcing.TransitiveGround.stageOneCollisionTest line 160
  23. def OAI.PartitionPilot.Forcing.TransitiveGround.stageOneSingleTests line 169
  24. def OAI.PartitionPilot.Forcing.TransitiveGround.stageOneTests line 178
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneCollisionTest_mono line 207
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneSingleTests_mono line 219
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneTests_mono line 228
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneTests_subset line 245
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneTests_empty line 258
  30. def OAI.PartitionPilot.Forcing.stageOneAssignmentUnion line 272
  31. theorem OAI.PartitionPilot.Forcing.mem_stageOneAssignmentUnion line 275
  32. theorem OAI.PartitionPilot.Forcing.stageOneAssignmentUnion_contains line 285
  33. theorem OAI.PartitionPilot.Forcing.stageOneAssignmentUnion_subset line 289
  34. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneTests_union line 309
  35. theorem OAI.PartitionPilot.Forcing.stageOneAssignmentUnion_raw_eq line 335
  36. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundSmallSubset_union_mem line 344