OAI/SetTheory/PartitionPrinciple/Transfinite/GroundRecursiveRefinementBinaryUnions.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Forcing.RecursiveRefinementDataHistory line 10
  2. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementDataHistory.carrier_entry line 22
  3. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementDataHistory.cut_mem line 28
  4. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementDataHistory.restrict line 39
  5. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementDataHistory.condition_iff_cuts line 59
  6. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementDataHistory.limit_eq line 98
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.forcingHistoryConditions_levels_congr line 119
  8. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementDataHistory.append line 134
  9. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementDataHistory.successor_eq line 152
  10. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementDataHistory.successor_insert_extension line 198
  11. structure OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory line 257
  12. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementDataHistory.cut_order line 267
  13. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.lower_order line 284
  14. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.restrict line 292
  15. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.append line 302
  16. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.restriction_successor_entry line 329
  17. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementDataHistory.stored_successor_eq line 359
  18. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementDataHistory.stored_successor_insert_extension line 372
  19. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.binary_union_mem_of_candidates line 418
  20. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.tests_at_valid_larger_cut line 505
  21. theorem OAI.PartitionPilot.Forcing.RecursiveRefinementOrderHistory.binary_union_extension line 549