OAI/SetTheory/PartitionPrinciple/Forcing/GroundGraphValueDescendantWitnesses.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rename_mem line 15
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.act_mem line 69
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceNameCandidates_act_iff line 99
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceNameCandidates_principal_act_iff line 113
  5. def OAI.PartitionPilot.Forcing.TransitiveGround.niceNameCandidateEquiv line 121
  6. theorem OAI.PartitionPilot.Forcing.Name.child_mem_doubleUnion line 145
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.separationName_mem line 159
  8. def OAI.PartitionPilot.Forcing.Name.immediateChildCodes line 212
  9. theorem OAI.PartitionPilot.Forcing.Name.mem_immediateChildCodes line 216
  10. theorem OAI.PartitionPilot.Forcing.Name.immediateChildCodes_valid line 232
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.immediateChildCodes_mem line 245
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.symmetricSeparationName_mem line 267
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.symmetric_separation line 295
  14. def OAI.PartitionPilot.Forcing.Name.childFamilyCodes line 325
  15. theorem OAI.PartitionPilot.Forcing.Name.mem_childFamilyCodes line 330
  16. theorem OAI.PartitionPilot.Forcing.Name.childFamilyCodes_valid line 353
  17. theorem OAI.PartitionPilot.Forcing.Name.childFamilyCodes_hs line 359
  18. theorem OAI.PartitionPilot.Forcing.Name.eval_member_childFamilyCodes line 370
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.childFamilyCodes_mem line 384
  20. def OAI.PartitionPilot.Forcing.Name.descendantFamilyCodes line 404
  21. theorem OAI.PartitionPilot.Forcing.Name.descendantFamilyCodes_valid line 408
  22. theorem OAI.PartitionPilot.Forcing.Name.descendantFamilyCodes_hs line 417
  23. theorem OAI.PartitionPilot.Forcing.Name.value_member_fourthDescendant line 430
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.descendantFamilyCodes_mem line 457
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.graphValue_fourthDescendant_dense line 479