OAI/SetTheory/PartitionPrinciple/Forcing/GroundMainFinalStructuralCommonSupportInduction.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BoundedFormula.separationWitnessBody line 14
  2. def OAI.PartitionPilot.Forcing.BoundedFormula.separationWitnessFormula line 19
  3. def OAI.PartitionPilot.Forcing.BoundedFormula.localizedWitnessFormula line 22
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.separationWitness_mem line 34
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.localized_mem line 91
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinary_generic_meets_coded_denseBelow line 146
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinary_generic_candidate_witness line 156
  8. def OAI.PartitionPilot.Forcing.SetFormula.rectangleOrderFormula line 179
  9. def OAI.PartitionPilot.Forcing.SetFormula.rectangleBodyFormula line 185
  10. def OAI.PartitionPilot.Forcing.SetFormula.rectangleWitnessFormula line 193
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.coded_action line 213
  12. def OAI.PartitionPilot.Forcing.TransitiveGround.rectangleParameters line 227
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_rectangleWitnessFormula line 232
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rectangleWitness_mem line 311
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.copyWitnessFamily_coded line 342
  16. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.internalRow_copyWitnessFamily_coded line 371
  17. theorem OAI.PartitionPilot.Forcing.GroundMainFinalGeometry.internalRow_copyWitness_generic line 426
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.forcesEq_mix_of_copy_refinements line 481
  19. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalFulfillment.structural_mixture_forcing line 544
  20. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.structural_dense_mixture_equalities line 765
  21. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.structural_common_support line 950
  22. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.structural_common_support_all_stages line 1152