OAI/SetTheory/PartitionPrinciple/Geometry/GroundCumulativeHierarchyLevels.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.SetFormula.cumulativeMemberFormula line 13
  2. def OAI.PartitionPilot.Forcing.SetFormula.cumulativeStepFormula line 18
  3. def OAI.PartitionPilot.Forcing.TransitiveGround.cumulativeNext line 28
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_cumulativeNext line 32
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_cumulativeMemberFormula line 42
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.cumulativeNext_mem line 69
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_cumulativeStepFormula line 95
  8. def OAI.PartitionPilot.Forcing.GroundCumulativeHierarchyCode line 130
  9. theorem OAI.PartitionPilot.Forcing.GroundCumulativeHierarchyCode.function line 136
  10. theorem OAI.PartitionPilot.Forcing.GroundCumulativeHierarchyCode.entry_iff line 138
  11. theorem OAI.PartitionPilot.Forcing.GroundCumulativeHierarchyCode.unique line 148
  12. theorem OAI.PartitionPilot.Forcing.GroundCumulativeHierarchyCode.restrict line 154
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundCumulativeHierarchy line 164
  14. theorem OAI.PartitionPilot.Forcing.GroundCumulativeHierarchyCode.mem_iff_rank_lt line 202
  15. theorem OAI.PartitionPilot.Forcing.GroundCumulativeHierarchyCode.value_transitive line 232
  16. theorem OAI.PartitionPilot.Forcing.GroundCumulativeHierarchyCode.value_mono line 239
  17. theorem OAI.PartitionPilot.Forcing.GroundCumulativeHierarchyCode.value_rank line 247
  18. theorem OAI.PartitionPilot.Forcing.GroundCumulativeHierarchyCode.zero_value line 256
  19. theorem OAI.PartitionPilot.Forcing.GroundCumulativeHierarchyCode.successor_value line 264
  20. theorem OAI.PartitionPilot.Forcing.GroundCumulativeHierarchyCode.limit_value line 283
  21. theorem OAI.PartitionPilot.Forcing.GroundCumulativeHierarchyCode.value_mem line 317
  22. theorem OAI.PartitionPilot.Forcing.GroundCumulativeHierarchyCode.ground_trace_iff line 321
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundCumulativeLevel line 345