OAI/SetTheory/PartitionPrinciple/Forcing/GroundNiceNameNormalization.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.Name.familySet line 13
  2. theorem OAI.PartitionPilot.Forcing.Name.entry_familySet line 17
  3. theorem OAI.PartitionPilot.Forcing.Name.familySet_code line 27
  4. theorem OAI.PartitionPilot.Forcing.Name.mem_eval_familySet line 41
  5. theorem OAI.PartitionPilot.Forcing.Name.act_familySet line 52
  6. theorem OAI.PartitionPilot.Forcing.Name.familySet_hs line 71
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.familySet_mem line 87
  8. theorem OAI.PartitionPilot.Forcing.Name.rename_familySet_of_encode line 107
  9. theorem OAI.PartitionPilot.Forcing.Name.eval_familySet_crossStage line 116
  10. theorem OAI.PartitionPilot.Forcing.Name.eval_crossStageMembershipName_of_decisions line 148
  11. theorem OAI.PartitionPilot.Forcing.Name.eval_crossStageMembershipName_of_subset line 180
  12. theorem OAI.PartitionPilot.Forcing.Name.eval_subset_familySet_of_code_subset line 201
  13. def OAI.PartitionPilot.Forcing.Name.niceNormalize line 220
  14. theorem OAI.PartitionPilot.Forcing.Name.entry_niceNormalize line 224
  15. theorem OAI.PartitionPilot.Forcing.Name.niceNormalize_subset line 236
  16. theorem OAI.PartitionPilot.Forcing.Name.eval_niceNormalize line 244
  17. theorem OAI.PartitionPilot.Forcing.Name.eval_niceNormalize_of_subset line 257
  18. theorem OAI.PartitionPilot.Forcing.Name.niceNormalize_niceNameCode line 272
  19. theorem OAI.PartitionPilot.Forcing.Name.niceNormalize_hs line 291
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.crossStageMembershipName_eval_of_family line 334
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.crossStageMembershipName_eval_of_family_subset line 371
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinarySeparationName_mem line 402
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceNormalize_mem line 418
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.entry_niceNormalize line 426
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceNormalize_spec line 438