OAI/SetTheory/PartitionPrinciple/Transfinite/RecursiveMaps.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.compose line 13
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.componentFilter line 20
  3. structure OAI.PartitionPilot.Compression.RecursiveMaps.Inputs line 27
  4. def OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.Eligible line 40
  5. def OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.Labels line 41
  6. def OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.nextBatch line 43
  7. def OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.freshImage line 60
  8. def OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.lift line 63
  9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.lift_old line 71
  10. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.lift_new_inside line 74
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.lift_new_outside line 78
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.fresh_shadow line 82
  13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.fresh_old_iff line 85
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.old_fresh_iff line 90
  15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.lift_agrees_on_base line 95
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.lift_template line 102
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.fresh_pair_iff line 114
  18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.meet_lift_old_old line 139
  19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.meet_lift_fresh_old line 152
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.meet_lift_template line 176
  21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.meet_lift_fresh_pair line 191
  22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.image_base_iff line 229
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.cut_identity line 249
  24. def OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.baseEmbedding line 261
  25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.meet_lift_with_base line 264
  26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.lift_preserves_meets line 274
  27. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.lift_monotone line 300
  28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.lift_reflects_order line 308
  29. def OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.liftedEmbedding line 340
  30. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.lift_injective line 345
  31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.fresh_below_cap line 348
  32. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.fresh_outside_base line 355
  33. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.range_below_cap line 360
  34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.Inputs.fresh_accounting line 365