OAI/SetTheory/PartitionPrinciple/Transfinite/LimitGroup.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem line 8
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.transition line 19
  3. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.Le line 24
  4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.le_stage line 27
  5. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.meet line 45
  6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.meet_stage line 48
  7. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.unionOrder line 52
  8. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.inclusion line 80
  9. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.boundedOrder line 85
  10. def OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.boundedInclusion line 87
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MeetSystem.bounded_strict_top line 90
  12. structure OAI.PartitionPilot.Compression.RecursiveMaps.GroupSystem line 97
  13. def OAI.PartitionPilot.Compression.RecursiveMaps.GroupSystem.transition line 108
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.GroupSystem.map_inv line 113
  15. def OAI.PartitionPilot.Compression.RecursiveMaps.GroupSystem.mul line 116
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.GroupSystem.mul_point line 119
  17. def OAI.PartitionPilot.Compression.RecursiveMaps.GroupSystem.inv line 123
  18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.GroupSystem.inv_point line 128
  19. def OAI.PartitionPilot.Compression.RecursiveMaps.GroupSystem.one line 133
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.GroupSystem.one_point line 135
  21. instance OAI.PartitionPilot.Compression.RecursiveMaps.GroupSystem.unionGroup line 140
  22. def OAI.PartitionPilot.Compression.RecursiveMaps.GroupSystem.inclusion line 161
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.GroupSystem.inclusion_injective line 166