OAI/SetTheory/PartitionPrinciple/Forcing/FixedTop.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.Le line 13
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.meet line 18
  3. def OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.order line 23
  4. def OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.embedding line 48
  5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.strict_top line 57
  6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.greatest line 60
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.no_new_below line 63
  8. def OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.act line 68
  9. def OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.actionIso line 72
  10. def OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.action line 92
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.fixes_top line 103
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.FixedTop.extends_action line 105
  13. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.Extension line 118
  14. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extensionOrder line 119
  15. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extensionAction line 120
  16. def OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extensionCopy line 122
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extension_greatest line 125
  18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extension_strict_top line 128
  19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extension_fixes_top line 133
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extensionAction_copy line 136
  21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extension_extends_old line 141
  22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.TileRequests.Family.extensionCopy_principal line 146