OAI/SetTheory/PartitionPrinciple/Forcing/GroundMixtureNames.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.SetFormula.realize_infinity_of_witness line 14
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.infinity_witness line 33
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.symmetric_infinity line 61
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.symmetric_ZF line 90
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_ZF_interpretation line 117
  6. def OAI.PartitionPilot.Forcing.Name.restrictBelow line 150
  7. theorem OAI.PartitionPilot.Forcing.Name.entry_restrictBelow line 152
  8. def OAI.PartitionPilot.Forcing.SetFormula.restrictionEntryFormula line 160
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_restrictionEntryFormula line 173
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.restrictBelow_mem line 217
  11. def OAI.PartitionPilot.Forcing.PosetAction.subgroupOrbitCodes line 259
  12. theorem OAI.PartitionPilot.Forcing.PosetAction.mem_subgroupOrbitCodes line 262
  13. theorem OAI.PartitionPilot.Forcing.PosetAction.entry_act_restrictBelow line 271
  14. theorem OAI.PartitionPilot.Forcing.PosetAction.mix_code_union line 290
  15. def OAI.PartitionPilot.Forcing.SetFormula.subgroupOrbitFormula line 322
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_subgroupOrbitFormula line 335
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.subgroupOrbitCodes_mem line 364
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mix_mem line 400