OAI/SetTheory/PartitionPrinciple/Forcing/NameRenameSteps.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.SetFormula.ordinaryGroundPrimitives line 9
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_ordinaryGroundForcing line 20
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryForcingSet_mem line 38
  4. def OAI.PartitionPilot.Forcing.SetFormula.candidateForcingFormula line 63
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_candidateForcingFormula line 82
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.candidateForcingSet_mem line 110
  7. def OAI.PartitionPilot.Forcing.Name.RenameStep line 145
  8. theorem OAI.PartitionPilot.Forcing.Name.rename_eq_step line 149
  9. theorem OAI.PartitionPilot.Forcing.Name.rename_postfixed_sound line 175
  10. theorem OAI.PartitionPilot.Forcing.Name.rename_prefixed_complete line 192
  11. def OAI.PartitionPilot.Forcing.SetFormula.ordinaryEqualityDecisionFormula line 219
  12. def OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryEqualityDecisions line 232
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryEqualityDecisions_subset line 236
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_ordinaryEqualityDecisionFormula line 242
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryEqualityDecisions_entry line 262
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryEqualityDecisions_dense line 275
  17. def OAI.PartitionPilot.Forcing.SetFormula.ordinaryMembershipDecisionFormula line 299
  18. def OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryMembershipDecisions line 312
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryMembershipDecisions_subset line 316
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_ordinaryMembershipDecisionFormula line 322
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryMembershipDecisions_entry line 342
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryMembershipDecisions_dense line 355