OAI/SetTheory/PartitionPrinciple/Geometry/CompatibleCopies.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data line 11
  2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.change_anchor_bound line 30
  3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.domain line 35
  4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.cocycle line 51
  5. def OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.Label line 66
  6. def OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.Related line 68
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.related_refl line 71
  8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.related_symm line 77
  9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.related_trans line 83
  10. def OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.setoid line 93
  11. def OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.Le line 97
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.le_refl line 100
  13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.related_le line 103
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.le_trans line 106
  15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.le_antisymm_related line 113
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.same_vertex_le line 120
  17. def OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.part line 127
  18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.part_anchor line 129
  19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.part_below line 132
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.below_iff_part line 138
  21. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CompatibleCopies.Data.move_to_upper_vertex line 148